This file contains some lemmas you will have to prove, i.e. replacing
the Admitted
joker with a sequence of tactic calls, terminated with a
Qed
command.
Each lemma should be proved several times : first using only elementary tactics : intros, apply, assumption split, left, right, destruct. exists, rewrite assert (only if you don't find another solution)
Then, use tactic composition, auto, tauto, firstorder.
Notice that, if you want to keep all solutions, you may use various identifiers like in the given example : imp_dist, imp_dist' share the same statement, with different interactive proofs.
Same exercise as the previous one, with full intuitionistic propositional logic
You may use the tactics intros, apply, assumption, destruct, left, right, split and try to use tactic composition