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.