Require Import List.
Require Import syntax.
Require Import environments.

Require Import utils.


Goal
forall (v x : vari) (t s : ty) (HF H : ty_env),
v <> x -> mapsto v t (HF ++ H) -> mapsto v t (HF ++ (x, s) :: H).

   simple induction HF; simpl in |- *.
   intros H neq M.
   apply F_If.
   red in |- *; intro; apply neq; symmetry in |- *; assumption.
   assumption.
   simple induction a; simpl in |- *; intros a0 b y IH H0 neq If.
   specialize (Xmidvar a0 v); simple induction 1. intro T.
   specialize If_T with (1 := If) (2 := T); intro B.
   apply T_If; assumption.
   intro F.
   specialize If_F with (1 := If) (2 := F); intro M.
   apply F_If. assumption.
   apply IH; assumption.
Save Mp_nfvExt.


Goal
forall (v x : vari) (t s : ty) (HF H : ty_env),
v <> x -> mapsto v t (HF ++ (x, s) :: H) -> mapsto v t (HF ++ H).

   simple induction HF; simpl in |- *.
   intros H neq If.
   apply If_F with (x = v) (s = t).
   assumption.
   red in |- *; intro; apply neq; symmetry in |- *; assumption.
   simple induction a; simpl in |- *; intros a0 b y IH H0 neq If.
   specialize (Xmidvar a0 v); simple induction 1. intro T.
   specialize If_T with (1 := If) (2 := T); intro B.
   apply T_If; assumption.
   intro F.
   specialize If_F with (1 := If) (2 := F); intro M.
   apply F_If. assumption.
   apply IH; assumption.
Save Mp_inv_nfvExt.


Goal
forall (x v : vari) (r s t : ty) (H HM H' : ty_env),
mapsto x t (H ++ (v, s) :: HM ++ H') ->
mapsto x t (H ++ (v, s) :: HM ++ (v, r) :: H').

   simple induction H; simpl in |- *.
   simple induction HM; simpl in |- *. intros.
   apply IfA_IfAIfA. assumption.
   simple induction a; simpl in |- *; intros.
   specialize (Xmidvar v x); simple induction 1.
   intro T.
   specialize If_T with (1 := H1) (2 := T); intro.
   apply T_If; assumption.
   intro F.
   specialize If_F with (1 := H1) (2 := F); intro I.
   apply F_If.
   assumption.
   specialize (Xmidvar a0 x); simple induction 1.
   intro Q.
   specialize If_T with (1 := I) (2 := Q); intro.
   apply T_If; assumption.
   intro nQ.
   specialize If_F with (1 := I) (2 := nQ); intro.
   apply F_If. assumption.
   apply If_F with (v = x) (s = t).
   apply H0.
   specialize If_F with (1 := H1) (2 := F); intro I2.
   specialize If_F with (1 := I2) (2 := nQ); intro.
   apply F_If; assumption.
   assumption.
   simple induction a; simpl in |- *; intros.
   specialize (Xmidvar a0 x); simple induction 1.
   intro T.
   specialize If_T with (1 := H1) (2 := T); intro.
   apply T_If; assumption.
   intro F.
   specialize If_F with (1 := H1) (2 := F); intro.
   apply F_If. assumption.
   apply H0; assumption.
Save Mp_eqExt.


Goal
forall (v x y : vari) (r s t : ty) (HF HM H : ty_env),
v = x ->
mapsto y r (HF ++ (v, s) :: HM ++ (x, t) :: H) ->
mapsto y r (HF ++ (v, s) :: HM ++ H).

   simple induction HF; simpl in |- *. intros HM H Q A.
   specialize (Xmidvar v y); simple induction 1. intro T.
   specialize If_T with (1 := A) (2 := T); intro sr.
   apply T_If; assumption.
   intro F.
   specialize If_F with (1 := A) (2 := F); intro M.
   apply F_If. assumption.
   apply Mp_inv_nfvExt with x t.
   elim Q; red in |- *; intro; apply F; symmetry in |- *; assumption.
   assumption.
   simple induction a; simpl in |- *; intros a0 b y0 IH HM H0 Q If.
   specialize (Xmidvar a0 y); simple induction 1. intro T.
   specialize If_T with (1 := If) (2 := T); intro br.
   apply T_If; assumption.
   intro F.
   specialize If_F with (1 := If) (2 := F); intro M.
   apply F_If. assumption.
   apply IH; assumption.
Save Mp_inv_eqExt.


Goal
forall (v x y : vari) (r s t : ty) (H H' : ty_env),
x <> y ->
mapsto v r (H ++ (x, s) :: (y, t) :: H') ->
mapsto v r (H ++ (y, t) :: (x, s) :: H').

        simple induction H.
        simpl in |- *; intros H' neq If.
        specialize (Xmidvar y v); simple induction 1.
        intro T.
        apply T_If. assumption.
        apply If_T with (y = v) (mapsto v r H').
        apply If_F with (x = v) (s = r).
        assumption.
        elim T; assumption.
        assumption.
        intro F.
        apply F_If. assumption.
        specialize (Xmidvar x v); simple induction 1.
        intro TT.
        specialize If_T with (1 := If) (2 := TT); intro sr.
        apply T_If; assumption.
        intro FF.
        specialize If_F with (1 := If) (2 := FF); intro If2.
        specialize If_F with (1 := If2) (2 := F); intro M.
        apply F_If; assumption.
        simple induction a.
        simpl in |- *; intros a0 b y0 IH H' N A.
        specialize (Xmidvar a0 v); simple induction 1.
        intro T.
        specialize If_T with (1 := A) (2 := T); intro br.
        apply T_If; assumption.
        intro F.
        specialize If_F with (1 := A) (2 := F); intro M.
        apply F_If; assumption || apply IH; assumption.
Save Mp_swap.