Definition and_i (A B:Prop) (a:A) (b:B):= (conj a b). Check and_i. Definition and_el (A B:Prop) (H:A/\B) := and_ind(fun (H0:A)(_:B)=>H0)H. Check and_el. Definition and_er (A B:Prop) (H:A/\B) := and_ind(fun (_:A)(H0:B)=>H0)H. Check and_er. Theorem or_il: forall A B:Prop, A->(A\/B). intro. trivial. auto. Save. Print or_il. Theorem or_ir: forall A B:Prop, B->(A\/B). intro. trivial. auto. Save. Print or_ir. Theorem or_e: forall A B C:Prop, (A\/B)->(A->C)->(B->C)->C. intros. elim H. trivial. auto. Save. Print or_e. Definition imp_i (A B:Prop) (x:A->B):= x. Definition imp_e (A B:Prop) (x:A->B) (y:A):= x y. (* Definition bot := forall B:Prop,B. *) Definition bot := False. Definition bot_e (A:Prop)(t:bot) := match t return A with end. (* Definition not (A:Prop) := A->bot. Definition neg_i (A:Prop)(t:not A):= t. Definition neg_e (A:Prop)(t:A)(u:not A):= u t. *) Definition neg_i (A:Prop)(t:not A):= t. Definition neg_e (A:Prop)(t:A)(u:not A):= u t. Definition copy (A:Prop)(t:A):= t. Theorem ex_e: forall iota:Set,forall P : iota-> Prop,forall t u, P t -> t=u ->P u. intros. rewrite <- H0. exact H. Defined. Ltac MP := fun A => apply (fun B=>fun u:A->B => fun y => u y). Ltac Felim := fun A => apply (fun t:A => t). Ltac Eelim := fun A => let H := fresh in (assert (H : A); [idtac|elim H;clear H;intro;intro]). Ltac Velim := fun A => let H := fresh in (assert (H:A); [idtac|elim H;clear H;intro]). Ltac Falseelim := let H := fresh in (assert (H:False);[idtac|induction H]). Ltac Notelim := fun A => let H := fresh in (assert (H:A); [idtac|let G := fresh in (assert (G:(not A)); [clear H | Falseelim ; exact (G H)])]). Ltac Aeliml := fun A => apply (fun B => fun u:(B/\A)=>fun v:((B/\A)->B)=> v u); [let H:=fresh in (intro H;let i:= fresh in let j:=fresh in (induction H as [i j];exact i)) |idtac]. Ltac Aelimr := fun A => apply (fun B => fun u:(A/\B)=>fun v:((A/\B)->B)=> v u); [let H:=fresh in (intro H;let i:= fresh in let j:=fresh in (induction H as [i j];exact j)) |idtac]. Ltac Rew := fun B t => apply (fun u H P=> eq_rect t B P u H). Ltac Eqelim := fun A B => match A with ?t=?u => Rew B t end. Ltac Swap := match goal with |- ?t=?u => Rew (fun x => x=u) u ;[reflexivity|idtac] end. Ltac Use := fun A => unfold A;fold A. Ltac Elim := fun A => match A with False => Falseelim | forall x,_ => Felim A | exists x,_ => Eelim A | _\/_ => Velim A | ~?S => Falseelim;Notelim S | left => (fun D => Aeliml D) | right => (fun D => Aelimr D) | ?S->_ => MP S | _=_ => (fun D => Eqelim A D) | _ => Falseelim;Notelim A end.