-lemma var_notinbG_notinG : \forall G,x,b.
- (\lnot (var_in_env x (b::G)))
- \to \lnot (var_in_env x G).
-intros 3.elim b.unfold.intro.elim H.unfold.simplify.constructor 2.exact H1.
-qed.
-
-lemma in_list_nil : \forall A,x.\lnot (in_list A x []).
-intros.unfold.intro.inversion H
- [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = [])
- [assumption|apply nil_cons]
- |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = [])
- [assumption|apply nil_cons]]
-qed.
-
-lemma notin_cons : \forall A,x,y,l.\lnot (in_list A x (y::l)) \to
- (y \neq x) \land \lnot (in_list A x l).
-intros.split
- [unfold;intro;apply H;rewrite > H1;constructor 1
- |unfold;intro;apply H;constructor 2;assumption]
-qed.
-
-lemma boundinenv_natinfv : \forall x,G.
- (\exists B,T.(in_list ? (mk_bound B x T) G)) \to
- (in_list ? x (fv_env G)).
-intros 2;elim G
- [elim H;elim H1;lapply (in_list_nil ? ? H2);elim Hletin
- |elim H1;elim H2;inversion H3
- [intros;rewrite < H4;simplify;apply in_Base
- |intros;elim a3;simplify;apply in_Skip;
- lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin in H;apply H;
- apply ex_intro
- [apply a
- |apply ex_intro
- [apply a1
- |rewrite > H6;assumption]]]]
-qed.
-
-lemma nat_in_list_case : \forall G,H,n.(in_list nat n (H @ G)) \to
- (in_list nat n G) \lor (in_list nat n H).
-intros 3.elim H
- [simplify in H1;left;assumption
- |simplify in H2;inversion H2
- [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;
- right;apply in_Base
- |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
- rewrite > H5 in H1;lapply (H1 H3);elim Hletin1
- [left;assumption|right;apply in_Skip;assumption]]]
-qed.
-
-lemma natinG_or_inH_to_natinGH : \forall G,H,n.
- (in_list nat n G) \lor (in_list nat n H) \to
- (in_list nat n (H @ G)).
-intros.elim H1
- [elim H
- [simplify;assumption
- |simplify;apply in_Skip;assumption]
- |generalize in match H2;elim H2
- [simplify;apply in_Base
- |lapply (H4 H3);simplify;apply in_Skip;assumption]]
-qed.
-
-lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to
- \exists B,T.(in_list ? (mk_bound B x T) G).
-intros 2;elim G 0
- [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin
- |intros 3;elim s;simplify in H1;inversion H1
- [intros;rewrite < H2;simplify;apply ex_intro
- [apply b
- |apply ex_intro
- [apply t
- |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin;
- apply in_Base]]
- |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
- rewrite < H4 in H2;lapply (H H2);elim Hletin1;elim H6;apply ex_intro
- [apply a2
- |apply ex_intro
- [apply a3
- |apply in_Skip;rewrite < H4;assumption]]]]
-qed.
-
-lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to
- (incl ? (fv_env l1) (fv_env l2)).
-intros.unfold in H.unfold.intros.apply boundinenv_natinfv.
-lapply (natinfv_boundinenv ? ? H1).elim Hletin.elim H2.apply ex_intro
- [apply a
- |apply ex_intro
- [apply a1
- |apply (H ? H3)]]
-qed.
-
-(* lemma incl_cons : \forall x,l1,l2.
- (incl bound l1 l2) \to (incl bound (x :: l1) (x :: l2)).
-intros.unfold in H.unfold.intros.inversion H1
- [intros;lapply (inj_head ? ? ? ? H3);rewrite > Hletin;apply in_Base
- |intros;apply in_Skip;apply H;lapply (inj_tail ? ? ? ? ? H5);rewrite > Hletin;
- assumption]
-qed. *)
-
-lemma incl_nat_cons : \forall x,l1,l2.
- (incl nat l1 l2) \to (incl nat (x :: l1) (x :: l2)).
-intros.unfold in H.unfold.intros.inversion H1
- [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base
- |intros;apply in_Skip;apply H;lapply (inj_tail ? ? ? ? ? H5);rewrite > Hletin;
- assumption]
-qed.
-
-lemma boundin_envappend_case : \forall G,H,b.(var_bind_in_env b (H @ G)) \to
- (var_bind_in_env b G) \lor (var_bind_in_env b H).
-intros 3.elim H
- [simplify in H1;left;assumption
- |unfold in H2;inversion H2
- [intros;simplify in H4;lapply (inj_head ? ? ? ? H4);rewrite > Hletin;
- right;apply in_Base
- |intros;simplify in H6;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
- rewrite > H5 in H1;lapply (H1 H3);elim Hletin1
- [left;assumption|right;apply in_Skip;assumption]]]
-qed.
-
-lemma varin_envappend_case: \forall G,H,x.(var_in_env x (H @ G)) \to
- (var_in_env x G) \lor (var_in_env x H).
-intros 3.elim H 0
- [simplify;intro;left;assumption
- |intros 2;elim s;simplify in H2;inversion H2
- [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;right;
- simplify;constructor 1
- |intros;lapply (inj_tail ? ? ? ? ? H6);
- lapply H1
- [rewrite < H5;elim Hletin1
- [left;assumption|right;simplify;constructor 2;assumption]
- |unfold var_in_env;unfold fv_env;rewrite > Hletin;rewrite > H5;
- assumption]]]
-qed.
-
-lemma boundinG_or_boundinH_to_boundinGH : \forall G,H,b.
- (var_bind_in_env b G) \lor (var_bind_in_env b H) \to
- (var_bind_in_env b (H @ G)).
-intros.elim H1
- [elim H
- [simplify;assumption
- |simplify;apply in_Skip;assumption]
- |generalize in match H2;elim H2
- [simplify;apply in_Base
- |lapply (H4 H3);simplify;apply in_Skip;assumption]]
-qed.
-
-
-lemma varinG_or_varinH_to_varinGH : \forall G,H,x.
- (var_in_env x G) \lor (var_in_env x H) \to
- (var_in_env x (H @ G)).
-intros.elim H1 0
- [elim H
- [simplify;assumption
- |elim s;simplify;constructor 2;apply (H2 H3)]
- |elim H 0
- [simplify;intro;lapply (in_list_nil nat x H2);elim Hletin
- |intros 2;elim s;simplify in H3;inversion H3
- [intros;lapply (inj_head_nat ? ? ? ? H5);rewrite > Hletin;simplify;
- constructor 1
- |intros;simplify;constructor 2;rewrite < H6;apply H2;
- lapply (inj_tail ? ? ? ? ? H7);rewrite > H6;unfold;unfold fv_env;
- rewrite > Hletin;assumption]]]
-qed.
-
-lemma varbind_to_append : \forall G,b.(var_bind_in_env b G) \to
- \exists G1,G2.(G = (G2 @ (b :: G1))).
-intros.generalize in match H.elim H
- [apply ex_intro [apply l|apply ex_intro [apply Empty|reflexivity]]
- |lapply (H2 H1);elim Hletin;elim H4;rewrite > H5;
- apply ex_intro
- [apply a2|apply ex_intro [apply (a1 :: a3)|simplify;reflexivity]]]
-qed.
-