+ |unfold;intros;elim (in_cons_case ? ? ? ? H9)
+ [rewrite > H10;apply in_Base
+ |elim H10;apply (in_Skip ? ? ? ? ? H11);apply (H7 ? H12)]]]
+qed.
+
+lemma decidable_eq_Typ : \forall S,T:Typ.(S = T) ∨ (S ≠ T).
+intro;elim S
+ [elim T
+ [elim (decidable_eq_nat n n1)
+ [rewrite > H;left;reflexivity
+ |right;intro;destruct H1;apply (H Hcut)]
+ |2,3:right;intro;destruct H
+ |*:right;intro;destruct H2]
+ |elim T
+ [2:elim (decidable_eq_nat n n1)
+ [rewrite > H;left;reflexivity
+ |right;intro;destruct H1;apply (H Hcut)]
+ |1,3:right;intro;destruct H
+ |*:right;intro;destruct H2]
+ |elim T
+ [3:left;reflexivity
+ |1,2:right;intro;destruct H
+ |*:right;intro;destruct H2]
+ |elim T
+ [1,2,3:right;intro;destruct H2
+ |elim (H t2)
+ [rewrite > H4;elim (H1 t3)
+ [rewrite > H5;left;reflexivity
+ |right;intro;apply H5;destruct H6;assumption]
+ |right;intro;apply H4;destruct H5;assumption]
+ |right;intro;destruct H4]
+ |elim T
+ [1,2,3:right;intro;destruct H2
+ |right;intro;destruct H4
+ |elim (H t2)
+ [rewrite > H4;elim (H1 t3)
+ [rewrite > H5;left;reflexivity
+ |right;intro;apply H5;destruct H6;assumption]
+ |right;intro;apply H4;destruct H5;assumption]]]