-lemma fv_env_extends : \forall H,x,B,C,T,U,G.
- (fv_env (H @ ((mk_bound B x T) :: G))) =
- (fv_env (H @ ((mk_bound C x U) :: G))).
-intros;elim H
- [simplify;reflexivity
- |elim s;simplify;rewrite > H1;reflexivity]
-qed.
-
-lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G.
- (WFEnv (H @ ((mk_bound B x T) :: G))) \to (WFType G U) \to
- (WFEnv (H @ ((mk_bound C x U) :: G))).
-intros 7;elim H 0
- [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1
- [intros;lapply (nil_cons ? G (mk_bound B x T));lapply (Hletin H4);
- elim Hletin1
- |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8);
- destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4;
- rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
- |intros;simplify;generalize in match H2;elim s;simplify in H4;
- inversion H4
- [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty)
- [assumption
- |apply nil_cons]
- |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);
- destruct Hletin1;apply WFE_cons
- [apply H1
- [rewrite > Hletin;assumption
- |assumption]
- |rewrite > Hcut1;generalize in match H7;rewrite < Hletin;
- rewrite > (fv_env_extends ? x B C T U);intro;assumption
- |rewrite < Hletin in H8;rewrite > Hcut2;
- apply (WFT_env_incl ? ? H8);rewrite > (fv_env_extends ? x B C T U);
- unfold;intros;assumption]]]
-qed.
-
-lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
- (in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G))) \to
- (y \neq x) \to
- (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
-intros 10;elim H
- [simplify in H1;(*FIXME*)generalize in match H1;intro;inversion H1
- [intros;lapply (inj_head ? ? ? ? H5);rewrite < H4 in Hletin;
- destruct Hletin;absurd (y = x) [symmetry;assumption|assumption]
- |intros;simplify;lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin;
- apply in_Skip;assumption]
- |(*FIXME*)generalize in match H2;intro;inversion H2
- [intros;simplify in H6;lapply (inj_head ? ? ? ? H6);rewrite > Hletin;
- simplify;apply in_Base
- |simplify;intros;lapply (inj_tail ? ? ? ? ? H8);rewrite > Hletin in H1;
- rewrite > H7 in H1;apply in_Skip;apply (H1 H5 H3)]]
-qed.
-
-lemma t_len_pred: \forall T,m.(S (t_len T)) \leq m \to (t_len T) \leq (pred m).
-intros 2;elim m
- [elim (not_le_Sn_O ? H)
- |simplify;apply (le_S_S_to_le ? ? H1)]
-qed.