NFP108 second devoir

Prouvez en déduction naturelle le lemme suivant:

((A=>B)/\((A/\B)\/(A\/B)))=>(~(A/\~B)/\ (A/\B)) \/(~(A/\~B)/\ (A\/B))

Pour simplifier les choses vous pouvez commencer par prouver les 2 lemmes suivants.

(A=>B) => ~(A/\~B)
A/\(B\/C)=>(A/\B)\/(A/\C)

Vous pouvez (devez ?) évidement utiliser le logiciel prévu pour vérifier chaque étape comme nous l'avons fait en TP. Vous fournirez un fichier texte contenant dans l'ordre la liste des règles utilisées; chaque règle etant éventuellement précéder de ces arguments.