- [intro;apply H7;apply natinG_or_inH_to_natinGH;right;assumption
- |intro;apply H7;apply natinG_or_inH_to_natinGH;left;assumption]]
- |apply (H2 H6)]]
-qed.
-
-(*** some exotic inductions and related lemmas ***)
-
-lemma O_lt_t_len: \forall T.O < (t_len T).
-intros;elim T
- [1,2,3:simplify;apply le_n
- |*:simplify;apply lt_O_S]
-qed.
-
-(*
-lemma not_t_len_lt_SO : \forall T.\lnot (t_len T) < (S O).
-intros;elim T
- [1,2,3:simplify;unfold;intro;unfold in H;elim (not_le_Sn_n ? H)
- |*:simplify;unfold;rewrite > max_case;elim (leb (t_len t) (t_len t1))
- [1,3:simplify in H2;apply H1;apply (trans_lt ? ? ? ? H2);unfold;constructor 1
- |*:simplify in H2;apply H;apply (trans_lt ? ? ? ? H2);unfold;constructor 1]]
-qed.
-*)
-
-lemma Typ_len_ind : \forall P:Typ \to Prop.
- (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V))
- \to (P U))
- \to \forall T.(P T).
-cut (\forall P:Typ \to Prop.
- (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V))
- \to (P U))
- \to \forall T,n.(n = (t_len T)) \to (P T))
- [intros;apply (Hcut ? H ? (t_len T));reflexivity
- |intros 4;generalize in match T;apply (nat_elim1 n);intros;
- generalize in match H2;elim t
- [1,2,3:apply H;intros;simplify in H4;elim (lt_to_not_le ? ? H4 (O_lt_t_len ?))
- |*:apply H;intros;apply (H1 (t_len V))
- [1,3:rewrite > H5;assumption
- |*:reflexivity]]]
-qed.
-
-lemma t_len_arrow1 : \forall T1,T2.(t_len T1) < (t_len (Arrow T1 T2)).
-intros.simplify.
-apply le_S_S.apply le_m_max_m_n.
-qed.
-
-lemma t_len_arrow2 : \forall T1,T2.(t_len T2) < (t_len (Arrow T1 T2)).
-intros.simplify.
-apply le_S_S.apply le_n_max_m_n.
-qed.
-
-lemma t_len_forall1 : \forall T1,T2.(t_len T1) < (t_len (Forall T1 T2)).
-intros.simplify.
-apply le_S_S.apply le_m_max_m_n.
-qed.
-
-lemma t_len_forall2 : \forall T1,T2.(t_len T2) < (t_len (Forall T1 T2)).
-intros.simplify.
-apply le_S_S.apply le_n_max_m_n.
-qed.
-
-lemma eq_t_len_TFree_subst : \forall T,n,X.(t_len T) =
- (t_len (subst_type_nat T (TFree X) n)).
-intro.elim T
- [simplify;elim (eqb n n1);simplify;reflexivity
- |2,3:simplify;reflexivity
- |simplify;lapply (H n X);lapply (H1 n X);rewrite < Hletin;rewrite < Hletin1;
- reflexivity
- |simplify;lapply (H n X);lapply (H1 (S n) X);rewrite < Hletin;
- rewrite < Hletin1;reflexivity]