Library HOC03CanonicalLemmas

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.


Definition XHE (f:height_fun) :=
  ∀ X X´ Y p, (f Y p) = (f ({{X,X´}}Y ) ({{[X,X´]}}p)).

Definition XHF (f:height_fun) :=
  ∀ X p, (f X p) \notin (E X p).

Definition XHP (f:height_fun) :=
  ∀ X Y p q, X≠Y → X#q → f X p = f X ([q//Y]p).

Definition good (f:height_fun) := (XHE f) ∧ (XHF f) ∧ (XHP f).


Fixpoint GoodF X P : nat :=
  match P with
    | Gvar Y ⇒ ifb (X=Y) then 1 else 0
    | Lvar _ ⇒ 0
    | Nil ⇒ 0
    | Par P1 P2 ⇒ max (GoodF X P1) (GoodF X P2)
    | Send a P ⇒ GoodF X P
    | Receive a x P ⇒ let m´ := GoodF X P in
      ifb (m´=0) then 0
        else ifb (x < m´) then m´
          else S x
end.

Lemma XHE_GoodF : XHE GoodF.
Proof.
  unfolds. induction p; simpls~; repeat cases_if¬.
  rewrite <- swap_gvar_equal_iff in e; tauto.
Qed.

Lemma Good0 : ∀ Y p, ifb (GoodF Y p = 0)
                          then Y \notin (GV p) else Y \in (GV p).
Proof.
  introv. inductions p; simpls; repeat cases_if¬.
  rewrite¬ in_singleton.
  unfold max in e; cases_if.
  rewrite e in l. false. nat_math.
  unfold max in e; cases_if.
  rewrite e in n0. false n0. nat_math.
  unfold max in e; cases_if.
  unfold max in n; cases_if.
  rewrite in_union. left¬.
  rewrite in_union. right¬.
  rewrite in_union. right¬.
Qed.

Lemma xEGood : ∀ x Y p, x \in (E Y p) → x < (GoodF Y p).
Proof.
  introv H. induction p; simpls*; unfolds lvar.
  cases_if. cases_if. rewrite <- e. apply IHp. rewrite¬ gfresh_E_empty.
  lets K: Good0. specialize (K Y p). cases_if¬.
    false n. unfolds¬.
    cases_if. cases_if. false. rewrite¬ <- (in_empty x).
  rewrite in_union in H. elim H.
    introv H1. rewrite in_singleton in H1. rewrite¬ H1.
    introv H1. applys¬ IHp.
  cases_if. false. erewrite <- in_empty. eassumption.
    rewrite in_union in H. elim H.
      introv H1. rewrite in_singleton in H1. rewrite H1. nat_math.
      introv H1. specialize (IHp H1). nat_math.
  rewrite× in_empty in H.
  cases_if; rewrite× in_empty in H.
  rewrite in_union in H. destruct H.
  unfold max. cases_if.
    specialize (IHp1 H). nat_math.
    applys¬ IHp1.
  unfold max. cases_if.
    applys¬ IHp2.
    specialize (IHp2 H). nat_math.
  rewrite in_empty in H. false.
Qed.

Lemma XHF_GoodF : XHF GoodF.
Proof.
  unfolds. introv HG. apply xEGood in HG. unfolds lvar; nat_math.
Qed.

Lemma GoodFresh : ∀ X Q, X # Q → GoodF X Q = 0.
Proof with freshen_up.
  inductions Q; introv Hf; simpls*; repeat cases_if×...
    false Hf. simpl. rewrite¬ in_singleton.
    unfold max; cases_if...
Qed.

Lemma GoodFresh_iff : ∀ X p, X # p ↔ GoodF X p = 0.
Proof with (freshen_up).
  introv; splits. apply GoodFresh.
    gen X. induction p using (measure_induction size); destruct p;
    introv Hf; simpl_fresh...
      apply¬ H; simpl; nat_math.
      simpls; repeat cases_if×.
      apply¬ H. nat_math.
      simpls; cases_if×.
      simpls. assert (GoodF X p1 = 0 ∧ GoodF X p2 = 0) by (unfold max in Hf; cases_if; nat_math).
      splits; apply H; nat_math.
Qed.

Lemma XHP_GoodF : XHP GoodF.
Proof.
  unfold XHP. introv HXY HXQ.
  inductions p; simpls*; repeat cases_if×.
    rewrite¬ <- IHp.
    false n. rewrite¬ <- IHp.
    rewrite <- e. applys¬ IHp.
    false n1. rewrite¬ <- IHp.
    false n. rewrite <- e. applys¬ IHp.
    false n0. rewrite¬ (IHp q).
    simpl. cases_if¬.
    symmetry. applys¬ GoodFresh.
    simpl. cases_if¬.
Qed.

Definition f := GoodF.

Theorem f_is_good : good f.
Proof.
  unfolds good. splits.
    apply XHE_GoodF.
    apply XHF_GoodF.
    apply XHP_GoodF.
Qed.

Opaque GoodF.


Lemma Good_chan_swap: ∀ p X m n, f X p = f X (|m,n|p).
Proof.
  induction p; simpls~; introv; repeat cases_if¬.
Qed.


Lemma Abs_eq : ∀ p a X Y, Y#p → Abs f a X p = Abs f a Y ([Gvar Y//X]p).
Proof.
  introv H. unfolds.
  assert (Hre: f Y ([Gvar Y//X]p) = f X p).
    rewrite gfresh_subst_is_swap.
      rewrite <- (swap_gvar_left X Y) at 1. symmetry. apply f_is_good.
      assumption.
  rewrite Hre. fequals.
  rewrite¬ (subst_decomposition_g X Y).
Qed.

Lemma subst_on_Abs : ∀ a X Y p r,
  X ≠ Y → X#r → [r//Y]Abs f a X p = Abs f a X ([r//Y]p).
  introv Hneq Hf. unfolds Abs. simpl.
  lets (_ & _ & XHP) : f_is_good. specialize (XHP X Y p r Hneq Hf).
  rewrite XHP. fequals.
  applys¬ subst_on_subst.
Qed.


Inductive wf : process → Prop :=
 | WfSend : ∀ (a:chan) (p:process), (wf p) → (wf (Send a p))
 | WfAbs : ∀ (a:chan) (X:var) (p:process), (wf p) → (wf (Abs f a X p))
 | WfGvar : ∀ (X:var), (wf (Gvar X))
 | WfPar : ∀ (p q : process), (wf p) → (wf q) → (wf (Par p q))
 | WfNil : (wf Nil).

Lemma my_wf_ind : ∀ (P : process → Prop),
  (∀ (a : chan) (p : process), wf p → P p → P (Send a p)) →
  (∀ (a : chan) (X : var) (p : process), wf p → P p → P (Abs f a X p)) →
  (∀ X : var, P (Gvar X)) →
  (∀ p q : process, wf p → P p → wf q → P q → P (Par p q)) →
  P Nil →
    ∀ p : process, wf p → P p.
Proof.
  introv HI1 HI2 HI3 HI4 HI5 Hwf.
  induction p using (measure_induction size). inverts Hwf.
    applys¬ HI1. applys¬ H. simpl. nat_math.
    unfold Abs in HI2. applys¬ HI2. applys¬ H. simpl. rewrite (size_subst).
      nat_math.
      simpls¬.
    exact (HI3 X).
    applys¬ HI4.
      applys¬H. simpl. nat_math.
      applys¬ H. simpl. nat_math.
    exact HI5.
Qed.

Lemma wf_send : ∀ a p, (wf (Send a p)) → wf p.
Proof.
  introv H; inverts¬ H.
Qed.

Lemma wf_LV : ∀ p,
  (wf p) → LV p = \{}.
Proof.
  induction 1 using my_wf_ind; simpls¬.
    assert (Has: ∀ x X p, (LV ([Lvar x // X]p) \- \{x}) \c (LV p)).
      introv. induction p0; simpls¬.
        rewrite remove_comm. applys¬ remove_in_subsets.
        unfold subset. introv H1. rewrite in_remove in H1. apply H1.
        cases_if×. simpl. lets H1: (remove_same \{x}). applys¬ fset_eq_sub.
        simpl. lets H1: (remove_from_empty \{x}). applys¬ fset_eq_sub.
        simpl. rewrite union_remove. applys¬ subset_union_2.
        simpl. lets H1: (remove_from_empty \{x}). applys¬ fset_eq_sub.
    specialize (Has (f X p) X p). apply subset_of_empty. rewrite¬ <- IHwf.
    rewrite IHwf1. rewrite IHwf2. rewrite¬ union_empty_l.
Qed.

Lemma wf_lfresh : ∀ x p,
  (wf p) → x##p.
Proof.
  introv Hwf. apply fresh_LV. applys¬ wf_LV.
Qed.

Lemma wf_par1 : ∀ p q, (wf (Par p q)) → (wf p).
Proof.
  introv H. inverts¬ H.
Qed.

Lemma wf_par2 : ∀ p q, (wf (Par p q)) → (wf q).
Proof.
  introv H. inverts¬ H.
Qed.

Lemma wf_swapping : ∀ p X X´, wf p → wf ({{[X, X´]}}p).
Proof.
  introv Hwf.
  induction Hwf using my_wf_ind; simpl; try constructor¬.
  forwards (XHE & _ & _): f_is_good. specialize (XHE X X´ X0 p).
  rewrite XHE. rewrite swap_on_subst. constructor¬.
Qed.

Lemma wf_chan_swap : ∀ p m n, wf p → wf (|m,n|p).
Proof.
  introv Hwf.
  induction Hwf using my_wf_ind; simpl; try constructor¬.
  rewrite swap_chan_on_subst. simpl.
  rewrite (Good_chan_swap p X m n); constructor¬.
Qed.

Lemma wf_prod_repeat : ∀ n p, wf p → wf (prod (repeat p n)).
Proof.
  induction n; introv H; simpl; constructor¬.
Qed.

Lemma wf_ind_gen : ∀ (P : process → Prop),
  (∀ a p, wf p → P p → P (Send a p)) →
  (∀ a X p, wf p → (∀ Y, Y#p → P ([Gvar Y//X]p)) → P (Abs f a X p)) →
  (∀ X, P (Gvar X)) →
  (∀ p q, wf p → P p → wf q → P q → P (Par p q)) →
  (P Nil) →
    ∀ p, wf p → P p.
Proof.
  introv HI1 HI2 HI3 HI4 HI5 Hwf.
  induction p using (measure_induction size). inverts× Hwf.
    applys¬ HI1. applys¬ H. simpl. nat_math.
    unfold Abs in HI2. applys¬ HI2. introv HF. applys¬ H.
      simpl. rewrite_all size_subst; simpls¬. nat_math.
      rewrite¬ gfresh_subst_is_swap. applys¬ wf_swapping.
    applys¬ HI4; applys¬ H; simpl; nat_math.
Qed.

Lemma wf_subst : ∀ p, wf p → ∀ X q, wf q → wf ([q//X]p).
Proof.
  introv Hwf1.
  elim Hwf1 using wf_ind_gen; intros; try constructor¬.
    lets (Y & Hf) : find_fresh (p0::q::(Gvar X)::(Gvar X0)::nil).
    rewrite Forall_to_conj_4 in Hf. destruct Hf as (Hfp & Hfq & HfX & HfX0).
    rewrite gfresh_gvar in HfX. rewrite gfresh_gvar in HfX0.
    rewrite¬ (Abs_eq p0 a X Y).
    rewrite¬ subst_on_Abs.
    constructor¬.
  simpls. cases_if¬. constructor.
Qed.

Lemma wf_receive : ∀ a x p, wf (Receive a x p) →
  ∀ X, X#p → wf ([Gvar X///x]p) ∧ Receive a x p = Abs f a X ([Gvar X///x]p).
Proof.
  introv Hwf Hf. split.
    inverts Hwf. rewrite <- subst_decomposition_l.
      applys¬ wf_subst. constructor.
      applys¬ wf_lfresh. apply f_is_good.
    inversion Hwf. subst a0. unfold Abs.
    assert (Heq: ([Gvar X /// x]([Lvar x // X0]p0)) = {{[X0,X]}}p0).
      etransitivity. symmetry. apply subst_decomposition_l.
      apply wf_LV in H0. unfold fresh_lvar. rewrite H0. apply notin_empty.
      rewrite <- H1. apply f_is_good.
      destruct (comparable X X0) as (b & dec). cases b.
      apply eq_true_l in dec. rewrite istrue_isTrue in dec.
      subst X0. rewrite swap_equal. apply subst_gvar_idem.
      apply eq_false_l in dec. rewrite istrue_neg in dec. rewrite istrue_isTrue in dec.
      apply gfresh_subst_is_swap. rewrite <- H2 in Hf. eapply gfresh_from_subst; eassumption.
    subst.
    rewrite Heq. assert (Heq2: f X ({{[X0, X]}}p0) = f X0 p0).
      symmetry. assert (Hre: X = {{X0, X}}X0).
        symmetry. apply swap_gvar_left.
      rewrite Hre at 1. apply f_is_good.
    rewrite Heq2. fequals. rewrite subst_on_swap.
    simpl. rewrite swap_gvar_right. symmetry.
  rewrite¬ swap_on_subst; simpl. rewrite swap_gvar_left.
    tests : (X = X0). rewrite¬ swap_equal.
    apply gfresh_from_subst in Hf; auto.
    rewrite <- Heq2. rewrite¬ <- gfresh_subst_is_swap.
    rewrite¬ <- subst_decomposition_g.
Qed.

Lemma wf_receive_part1 : ∀ a x p, wf (Receive a x p) → ∀ X, X#p → wf ([Gvar X///x]p).
Proof.
  introv Hwf; introv Hf; lets H : (wf_receive a x p Hwf X Hf); tauto.
Qed.


Record wfprocess : Set := mkWfP {proc :> process; wf_cond : wf proc}.

Hint Resolve wf_cond.

Lemma wfprocess_eq : ∀ (p q : wfprocess), p = q ↔ proc p = proc q.
Proof.
intros p´ q´; split.

intro H; rewrite H; auto.

elim p´; elim q´; intros procP wP procQ wQ H; simpl in H.
generalizes wQ wP; rewrite H; intros wP wQ.
assert (Heq_wP_wQ : wP = wQ) by (apply proof_irrelevance).
rewrite Heq_wP_wQ; reflexivity.
Qed.


Definition wfp_Send m (p : wfprocess) := mkWfP (Send m p) (WfSend m p (wf_cond p)).
Definition wfp_Abs a X (p : wfprocess) := mkWfP (Abs f a X p) (WfAbs a X p (wf_cond p)).
Definition wfp_Gvar X := mkWfP (Gvar X) (WfGvar X).
Definition wfp_Par (p q : wfprocess) :=
  mkWfP (Par p q) (WfPar p q (wf_cond p) (wf_cond q)).
Definition wfp_Nil := mkWfP (Nil) (WfNil).

Definition wfp_subst (q : wfprocess) X (p : wfprocess) :=
  mkWfP ([q//X]p) (wf_subst p (wf_cond p) X q (wf_cond q)).


Ltac rewrite_wfp_equal := rewrite wfprocess_eq; simpls¬.

Ltac rewrite_into_wfp :=
match goal with
 
 | [ |- context[mkWfP (Send ?a ?p) ?wfCond]] ⇒
   match goal with
     | [ H : wf p |- _ ] ⇒
       replace (mkWfP (Send a p) wfCond) with (wfp_Send a (mkWfP p H))
       in × by rewrite_wfp_equal
     | [ p : wfprocess |- _ ] ⇒
       replace (mkWfP (Send a p) wfCond) with (wfp_Send a (mkWfP p (wf_cond p)))
       in × by rewrite_wfp_equal
   end
 
 | [ |- context[mkWfP (Abs ?f ?a ?X ?p) ?wfCond]] ⇒
   match goal with
     | [ H : wf p |- _ ] ⇒
       replace (mkWfP (Abs f a X p) wfCond) with (wfp_Abs a X (mkWfP p H))
       in × by rewrite_wfp_equal
     | [ p : wfprocess |- _ ] ⇒
       replace (mkWfP (Abs f a X p) wfCond) with (wfp_Abs a (mkWfP p (wf_cond p)))
       in × by rewrite_wfp_equal
   end
 
 | [ |- context[mkWfP (Receive ?a (?f ?X ?p) ([Lvar (?f ?X ?p) // ?X]?p)) ?wfCond]] ⇒
   match goal with
     | [ H : wf p |- _ ] ⇒
       replace (mkWfP (Receive a (f X p) ([Lvar (f X p) // X]p)) wfCond)
       with (wfp_Abs a X (mkWfP p H))
       in × by rewrite_wfp_equal
     | [ p : wfprocess |- _ ] ⇒
       replace (mkWfP (Receive a (f X p) ([Lvar (f X p) // X]p)) wfCond)
       with (wfp_Abs a X (mkWfP p (wf_cond p)))
       in × by rewrite_wfp_equal
   end
 
 | [ |- context[mkWfP (Gvar ?X) ?wfCond]] ⇒
   replace (mkWfP (Gvar X) wfCond) with (wfp_Gvar X)
   in × by rewrite_wfp_equal
 
 | [ |- context[mkWfP (Par ?p ?q) ?wfCond]] ⇒
   match goal with
     | [ Hp : wf p, Hq : wf q |- _ ] ⇒
       replace (mkWfP (Par p q) wfCond) with (wfp_Par (mkWfP p Hp) (mkWfP q Hq))
       in × by rewrite_wfp_equal
     | [ p : wfprocess, Hq : wf q |- _ ] ⇒
       replace (mkWfP (Par p q) wfCond)
       with (wfp_Par (mkWfP p (wf_cond p)) (mkWfP q Hq))
       in × by rewrite_wfp_equal
     | [ Hp : wf p, Hq : wf q |- _ ] ⇒
       replace (mkWfP (Par p q) wfCond) with (wfp_Par (mkWfP p Hp) (mkWfP q Hq))
       in × by rewrite_wfp_equal
     | [ Hp : wf p, q : wfprocess |- _ ] ⇒
       replace (mkWfP (Par p q) wfCond)
       with (wfp_Par (mkWfP p Hp) (mkWfP q (wf_cond q)))
       in × by rewrite_wfp_equal
     | [ p : wfprocess, q : wfprocess |- _ ] ⇒
       replace (mkWfP (Par p q) wfCond)
       with (wfp_Par (mkWfP p (wf_cond p)) (mkWfP q (wf_cond q)))
       in × by rewrite_wfp_equal
   end
 
 | [ |- context[mkWfP Nil ?wfCond]] ⇒
   replace (mkWfP Nil wfCond) with (wfp_Nil)
   in × by rewrite_wfp_equal
end.


Definition wfp_size (p : wfprocess) : nat := size (proc p).

Ltac solve_wfp_size :=
  try match goal with
    | [ |- wfp_size _ < wfp_size (wfp_Abs _ _ _) ] ⇒
      unfold wfp_size in *; simpls; repeat rewrite¬ size_subst; nat_math
    | [ |- wfp_size _ = wfp_size (wfp_Abs _ _ _) ] ⇒
      unfold wfp_size in *; simpls; repeat rewrite¬ size_subst; nat_math
    | [ |- wfp_size (wfp_Abs _ _ _) = wfp_size _ ] ⇒
      unfold wfp_size in *; simpls; repeat rewrite¬ size_subst; nat_math
  end;
  try (unfold wfp_size in *; simpls; nat_math).

Definition wfp_sizeP (p : wfprocess) : nat := sizeP (proc p).

Ltac solve_wfp_sizeP :=
  try match goal with
    | [ |- wfp_sizeP _ < wfp_sizeP (wfp_Abs _ _ _) ] ⇒
      unfold wfp_sizeP in *; simpls; repeat rewrite¬ sizeP_subst; nat_math
    | [ |- wfp_sizeP _ = wfp_sizeP (wfp_Abs _ _ _) ] ⇒
      unfold wfp_sizeP in *; simpls; repeat rewrite¬ sizeP_subst; nat_math
    | [ |- wfp_sizeP (wfp_Abs _ _ _) = wfp_sizeP _ ] ⇒
      unfold wfp_sizeP in *; simpls; repeat rewrite¬ sizeP_subst; nat_math
  end;
  try (unfold wfp_sizeP in *; simpls; nat_math).


Lemma wfp_ind : ∀ (P : wfprocess → Prop),
  (∀ (a : chan) (p : wfprocess), P p → P (wfp_Send a p)) →
  (∀ (a : chan) (X : var) (p : wfprocess), P p → P (wfp_Abs a X p)) →
  (∀ X : var, P (wfp_Gvar X)) →
  (∀ p q : wfprocess, P p → P q → P (wfp_Par p q)) →
  P wfp_Nil →
    ∀ p : wfprocess, P p.
Proof with solve_wfp_size.
introv HSend HAbs HGvar HPar HNil.
induction p using (measure_induction wfp_size).

induction p; rename proc0 into p.
induction p; inversion wf_cond0; subst; try rewrite_into_wfp; auto.
  applys¬ HSend; apply H...
  applys¬ HAbs; apply H...
  applys¬ HPar; apply H...
Qed.

Lemma wf_characterize : ∀ p : wfprocess,
  (∃ a p´, p = wfp_Send a p´) ∨
  (∃ a X p´, p = wfp_Abs a X p´) ∨
  (∃ X, p = wfp_Gvar X) ∨
  (∃ p1 p2, p = wfp_Par p1 p2) ∨
  p = wfp_Nil.
Proof.
  induction p using wfp_ind.
    branch 1. ∃¬ a p.
    branch 2. ∃¬ a X p.
    branch 3. ∃¬ X.
    branch 4. ∃¬ p1 p2.
    branch 5. auto.
Qed.

Ltac destruct_wf q :=
  let p := fresh "p" in
  let a := fresh "a" in
  let X := fresh "X" in
  let p1 := fresh "p1" in
  let p2 := fresh "p2" in
  let Hyp := fresh "Hyp" in
    destruct (wf_characterize q) as
      [[a [p Hyp]] |
      [[a [X [p Hyp]]] |
      [[X Hyp] |
      [[p1 [p2 Hyp]] | ]]]]; subst q.

Lemma wfp_ind_gen : ∀ (P : wfprocess → Prop),
  (∀ a p, P p → P (wfp_Send a p)) →
  (∀ a X (p : wfprocess), (∀ Y, Y#p → P (wfp_subst (wfp_Gvar Y) X p)) → P (wfp_Abs a X p)) →
  (∀ X, P (wfp_Gvar X)) →
  (∀ p q, P p → P q → P (wfp_Par p q)) →
  (P wfp_Nil) →
    ∀ p, P p.
Proof with (solve_wfp_size).
  introv HI1 HI2 HI3 HI4 HI5.
  induction p using (measure_induction wfp_size).
  destruct_wf p; jauto.
    applys¬ HI1. applys¬ H...
    apply HI2. introv Hf; apply H...
    applys¬ HI4; applys¬ H...
Qed.

Hint Resolve WfSend WfAbs WfGvar WfPar WfNil wf_subst wf_lfresh.


Require Import Recdef.

Function check_wf_bool (p : process) {measure size}: bool :=
  match p with
    | Send _ p ⇒ check_wf_bool p
    | Receive _ x p ⇒ (let X := var_gen (GV p) in
                         (isTrue (x = f X ([Gvar X /// x]p)) && check_wf_bool ([Gvar X /// x]p)))
    | Lvar x ⇒ false
    | Gvar _ ⇒ true
    | Par p q ⇒ (check_wf_bool p) && (check_wf_bool q)
    | Nil ⇒ true
  end.
introv _; simpl; nat_math.
introv _. rewrite¬ <- size_lsubst.
introv _; simpl; nat_math.
introv _; simpl; nat_math.
Defined.

Instance wf_decidable : ∀ p, Decidable (wf p).
Proof with (repeat rewrite istrue_isTrue in *; jauto).
  introv.
  applys¬ decidable_make (check_wf_bool p).
  induction p using (measure_induction size).
  rewrite check_wf_bool_equation; destruct p; extens; splits; introv Hyp; simpls...
    rewrite H in Hyp... constructor¬. nat_math.
    rewrite H... inverts¬ Hyp. nat_math.

    rewrite istrue_and in Hyp.
    destruct Hyp as (Heql & Hwf)...
    remember (var_gen (GV p)) as X.
    rewrite <- (subst_lvar_idem l p).
    rewrite lsubst_decomposition_g with (X := X).
    rewrite Heql at 1 2. constructor.
    rewrite¬ H in Hwf...
    rewrite¬ <- size_lsubst; nat_math.
    subst X. lets H1 : var_gen_spec (GV p).
    unfolds¬ fresh_gvar.

    rewrite istrue_and...
    remember (var_gen (GV p)) as X.
    apply wf_receive with (X := X) in Hyp.
    destruct Hyp as (Hwf & Heq).
    unfold Abs in *; splits.
      inverts¬ Heq; repeat rewrite <- H2; rewrite <- H1; auto.
      rewrite¬ H... rewrite¬ <- size_lsubst; nat_math.
      subst X. lets H1 : var_gen_spec (GV p).
      unfolds¬ fresh_gvar.

    inverts Hyp.
    inverts Hyp.

    rewrite istrue_and in Hyp...
    inverts Hyp; constructor; rewrite H in *; try nat_math...
    rewrite istrue_and. inverts Hyp; split; rewrite H; try nat_math...
Qed.