Section Base_Definitions.

   Section inductive_sets.

      Inductive Set Empty := .

      Inductive Set List [S:Set] := empty: (List S) | fr: (List S) -> S -> (List S).

      Inductive Id [S:Set; a:S]: S -> Set := id_r: (Id S a a).

      Inductive Set Pi [S:Set; P:S->Set] := abst: ((a:S) (P a)) -> (Pi S P).

      Inductive Set Sigma [S:Set; P:S->Set] := pair: (a:S) (P a) -> (Sigma S P).
      
      Inductive Set Plus [S,T:Set] := in_l : S -> (Plus S T) | in_r : T -> (Plus S T). 
(*      
Inductive SId [A:Set] : Set -> Set := sid_r: (SId A A).
*)
   End inductive_sets.
   
   Section eliminators.

      Definition efq := Empty_rec.

      Definition listrec := List_rec.

      Definition idrec := Id_rec.

      Definition fsplit := Pi_rec.

      Definition psplit := Sigma_rec.

      Definition when := Plus_rec.
      
      Definition EmptyFam := Empty_rect.

      Definition ListFam := List_rect.
      
      Definition IdFam := Id_rect.
      
      Definition PiFam := Pi_rect.
      
      Definition SigmaFam := Sigma_rect.

      Definition PlusFam := Plus_rect.

      Definition ap: (S:Set; P:S->Set) (Pi S P) -> (a:S) (P a).
      Intros.
      Elim H.
      Intros.
      Apply (p a).
      Defined.

      Definition sp: (S:Set; P:S->Set) (Sigma S P) -> S.
      Intros.
      Elim H.
      Intros.
      Assumption.
      Defined.

      Definition sq: (S:Set; P:S->Set; p:(Sigma S P)) (P (sp S P p)).
      Intros.
      Elim p.
      Intros.
      Unfold sp.
      Simpl.
      Assumption.
      Defined.

   End eliminators.

   Section functions.
   
      Definition id: (S:Set) S -> S.
      Intros.
      Assumption.
      Defined.

      Definition comp: (R,S,T:Set) (R -> S) -> (S -> T) -> (R -> T).
      Intros.
      Apply H0.
      Apply H.
      Assumption.
      Defined.

   End functions.

End Base_Definitions.

Section Base_Results.

   Section general_results.

      Theorem mcut: (S,T:Set) S -> (S -> T) -> T.
      Intros.
      Apply H0.
      Assumption.
      Qed.

   End general_results.

   Section ID_results.

      Theorem id_repl: (S:Set; a,b:S; P:S->Set) (Id ? b a) -> (P b) -> (P a).
      Intros.
      Elim H.
      Assumption.
      Qed.

      Theorem id_comm: (S:Set; a,b:S) (Id ? b a) -> (Id ? a b).
      Intros.
      Apply (id_repl S a b).
      Assumption.
      Apply id_r.
      Qed.
   
      Theorem id_trans: (S:Set; c,a,b:S) (Id S a c) -> (Id S c b) -> (Id S a b).
      Intros.
      Apply (id_repl S b c).
      Assumption.
      Assumption.
      Qed.

      Theorem id_comp: (S,T:Set; f:S->T; a,b:S) (Id S a b) -> (Id T (f a) (f b)).
      Intros.
      Apply (id_repl ? b a).
      Assumption.
      Apply id_r.
      Qed.
   
      Axiom id_ext: (S,T:Set; f,g:S->T) ((a:S) (Id T (f a) (g a))) -> (Id S->T f g).
   
   End ID_results.
(*
Section SID_results.

Theorem sid_repl: (A,B:Set; P:Set->Set) (SId B A) -> (P B) -> (P A).
Intros.
Elim H.
Assumption.
Qed.

Theorem sid_comp: (P:Set->Set; A,B:Set) (SId A B) -> (SId (P A) (P B)).
Intros.
Apply (sid_repl B A).
Assumption.
Apply sid_r.
Qed.

Axiom sid_ext: (S:Set; P:(S->Set)->Set; Q,R:S->Set) ((a:S) (SId (Q a) (R a))) -> (SId (P Q) (P R)).

End SID_results.
*)
   Section indipendence.
   
      Axiom list_p4: (S:Set; l:(List S); a:S) (Id (List S) (empty S) (fr S l a)) -> Empty.

      Axiom plus_p4: (S:Set; a:S; T:Set; b:T) (Id (Plus S T) (in_l S T a) (in_r S T b)) -> Empty.
(*
Axiom id_ctt: (S:Set) (P:(a:S)(Id S a a) -> Set) ((a:S) (P a (id_r S a))) -> (a:S; p:(Id S a a)) (P a p). 
*)   
   End indipendence.

End Base_Results.

Tactic Definition MTrivial := Try Apply id_r; (* Try Apply sid_r; *) 
(*|*)                         Try Assumption; Try Apply id_comm; 
                              Try Assumption; Try Apply id_comm.

Tactic Definition MFold := Idtac. 

Tactic Definition MRed := Idtac.

Tactic Definition MAuto := MTrivial; MFold; MRed.

Tactic Definition MSimpl := Simpl; MAuto.

Tactic Definition MElim v e := Pattern v; Elim v using e; Simpl; 
                               Intros; MAuto.

Tactic Definition MApply t := Apply t; Intros; MTrivial.

Tactic Definition MCut t := MApply '(mcut t).

Tactic Definition UnIntros T t := Apply (mcut T); Try Assumption; Clear t.