Library substLemmas

Require Import language.

Lemma AsubstValEquivA: forall E A s v x, (AEval A s) = Some v ->
AEval (ASubstA (E) A x) s = AEval (ASubstA (E) (IntExpr v) x) s.
intros.
induction E using AExpr_ind_mut with (P:= fun H =>
(AEval A s) = Some v -> HEval (HSubstA H A x) s = HEval (HSubstA H (IntExpr v) x) s);
intros. auto. auto. simpl. erewrite IHE2; eauto. erewrite IHE3; eauto. erewrite IHE1; eauto.

simpl. remember (beq_SkalVar x (ASkalVar a)). destruct b. rewrite H. auto.
auto. auto.

simpl in *.

assert (AEval (ASubstA E1 A x) s = AEval (ASubstA E1 (IntExpr v) x) s); auto.
assert (AEval (ASubstA E2 A x) s = AEval (ASubstA E2 (IntExpr v) x) s); auto.
remember (AEval (ASubstA E1 A x) s). destruct o.
remember ( AEval (ASubstA E1 (IntExpr v) x) s). destruct o.

remember (AEval (ASubstA E2 A x) s). destruct o.
remember ( AEval (ASubstA E2 (IntExpr v) x) s). destruct o.

inv H1. inv H0. auto. inv H1. destruct (AEval (ASubstA E2 (IntExpr v) x) s).
inv H1. auto. destruct (AEval (ASubstA E2 A x) s). inv H0. auto.
destruct (AEval (ASubstA E1 (IntExpr v) x) s). destruct (AEval (ASubstA E2 (IntExpr v) x) s).
inv H0. auto. auto.

simpl in *.
assert (AEval (ASubstA E A x) s = AEval (ASubstA E (IntExpr v) x) s).
apply IHE0; auto.
assert (HEval (HSubstA h A x) s = HEval (HSubstA h (IntExpr v) x) s).
apply IHE; eauto.
destruct (AEval (ASubstA E A x) s). destruct (AEval (ASubstA E (IntExpr v) x) s).
inv H0.
destruct (HEval (HSubstA h A x) s). destruct (HEval (HSubstA h (IntExpr v) x) s).
inv H1. auto. inv H1. destruct (HEval (HSubstA h (IntExpr v) x) s). inv H1. auto. inv H0.
destruct (AEval (ASubstA E (IntExpr v) x) s). inv H0. auto.
Qed.

Lemma BsubstValEquivB: forall B s v E x, (BEval B s) = Some v ->
BEval (BSubstB (E) B x) s = BEval (BSubstB (E) (BvalExpr v) x) s.
intros. induction E. simpl. remember (beq_SkalVar x (BSkalVar b)). destruct b0. rewrite H. auto.
auto. auto.

simpl. auto. simpl. rewrite IHE1. rewrite IHE2. auto. simpl. rewrite IHE1. rewrite IHE2. auto.
simpl. rewrite IHE. auto.
Qed.

Lemma HsubstValEquivA: forall E A s v x, (AEval A s) = Some v ->
HEval (HSubstA (E) A x) s = HEval (HSubstA (E) (IntExpr v) x) s.
intros.
induction E using HExpr_ind_mut with (P0:= fun H =>
(AEval A s) = Some v -> AEval (ASubstA H A x) s = AEval (ASubstA H (IntExpr v) x) s);
intros. auto. auto. simpl. erewrite IHE1; eauto. erewrite IHE0; eauto. erewrite IHE; eauto.

simpl. destruct (beq_SkalVar x (ASkalVar a)). auto. auto.

auto.

simpl. rewrite IHE; auto. rewrite IHE0; auto.

simpl. rewrite IHE; auto. rewrite IHE0; auto.
Qed.

Lemma hValToExprSound: forall v s, HEval (hValToHExpr v) s=Some v.
Proof.
intros. induction v. auto.
simpl. destruct a. simpl in *. rewrite IHv. auto.
Qed.

Lemma AsubstValEquivH: forall E H s v x, (HEval H s) = Some v ->
AEval (ASubstH (E) H x) s = AEval (ASubstH (E) (hValToHExpr v) x) s.
intros.
induction E using AExpr_ind_mut with (P:= fun A =>
(HEval H s) = Some v -> HEval (HSubstH A H x) s = HEval (HSubstH A (hValToHExpr v) x) s);
intros; auto.
simpl. remember (beq_SkalVar x (HSkalVar h)). destruct b. rewrite hValToExprSound.
auto.
auto.

simpl in *.

specialize (IHE1 H0).
rewrite IHE1. rewrite IHE2. rewrite IHE3. auto.

simpl.
rewrite <- IHE1. rewrite <- IHE2. auto.

simpl in *. specialize (IHE H0).
rewrite IHE. rewrite IHE0.
auto.

Qed.

Lemma HsubstValEquivH: forall E H s v x, (HEval H s) = Some v ->
HEval (HSubstH E H x) s = HEval (HSubstH E (hValToHExpr v) x) s.
Proof.
intros.
induction E; auto. simpl. remember (beq_SkalVar x (HSkalVar h)). destruct b.
rewrite hValToExprSound. auto.

auto. simpl in *. remember (HEval (HSubstH E H x) s).
remember (HEval (HSubstH E (hValToHExpr v) x) s).
rewrite AsubstValEquivH with (v:=v).
rewrite (AsubstValEquivH a0 H) with (v:=v).
destruct o; destruct o0; inv IHE. auto. auto. auto.
auto.
Qed.

Lemma BsubstValEquivA: forall A s v E x, (AEval A s) = Some v -> BEval (BSubstA (E) A x) s = BEval (BSubstA (E) (IntExpr v) x) s.
Proof. intros. induction E. auto. auto.

simpl. rewrite AsubstValEquivA with (v:=v). rewrite (AsubstValEquivA a0 _ _ v _). auto. auto. auto.

simpl in IHE1. simpl. simpl in IHE2.
remember (BEval (BSubstA E1 A x) s). destruct o.
remember (BEval (BSubstA E1 (IntExpr v) x) s). destruct o.
remember (BEval (BSubstA E2 A x) s). destruct o.
remember (BEval (BSubstA E2 (IntExpr v) x) s). destruct o.
inv IHE2. inv IHE1. auto. inv IHE2.
remember (BEval (BSubstA E2 (IntExpr v) x) s). destruct o. inv IHE2.
auto. inv IHE1.
remember (BEval (BSubstA E1 (IntExpr v) x) s). destruct o. inv IHE1. auto.

simpl in IHE1. simpl. simpl in IHE2.
remember (BEval (BSubstA E1 A x) s). destruct o.
remember (BEval (BSubstA E1 (IntExpr v) x) s). destruct o.
remember (BEval (BSubstA E2 A x) s). destruct o.
remember (BEval (BSubstA E2 (IntExpr v) x) s). destruct o.
inv IHE2. inv IHE1. auto. inv IHE2.
remember (BEval (BSubstA E2 (IntExpr v) x) s). destruct o. inv IHE2.
auto. inv IHE1.
remember (BEval (BSubstA E1 (IntExpr v) x) s). destruct o. inv IHE1. auto.

simpl in IHE.
remember (BEval (BSubstA E A x) s). destruct o.
remember (BEval (BSubstA E (IntExpr v) x) s). destruct o.
inv IHE. simpl. inv Heqo0. inv Heqo. auto. inv Heqo0. inv IHE.
remember (BEval (BSubstA E (IntExpr v) x) s). destruct o. inv IHE.
simpl. inv Heqo. inv Heqo0. auto.

Qed.

Lemma BsubstValEquivH: forall H s v E x, (HEval H s) = Some v ->
BEval (BSubstH (E) H x) s = BEval (BSubstH (E) (hValToHExpr v) x) s.
Proof.
intros.
induction E; auto.
simpl. rewrite AsubstValEquivH with (v:=v) by auto.
rewrite (AsubstValEquivH a0) with (v:=v); auto.
simpl.
remember (BEval (BSubstH E1 H x) s).
remember (BEval (BSubstH E1 (hValToHExpr v) x) s).
remember (BEval (BSubstH E2 H x) s).
remember (BEval (BSubstH E2 (hValToHExpr v) x) s).
destruct o; destruct o0; inversion IHE1; destruct o1; destruct o2; inv IHE2; auto.

simpl.
remember (BEval (BSubstH E1 H x) s).
remember (BEval (BSubstH E1 (hValToHExpr v) x) s).
remember (BEval (BSubstH E2 H x) s).
remember (BEval (BSubstH E2 (hValToHExpr v) x) s).
destruct o; destruct o0; inversion IHE1; destruct o1; destruct o2; inv IHE2; auto.

simpl.

destruct (BEval (BSubstH E H x) s);
destruct (BEval (BSubstH E (hValToHExpr v) x) s); inv IHE; auto.
Qed.

Lemma substValEquivA: forall A s v E x, (AEval A s) = Some v -> Eval (SubstA E A x) s = Eval (SubstA E (IntExpr v) x) s.
intros. destruct E. simpl. rewrite AsubstValEquivA with (v:=v). auto. auto.
simpl. rewrite BsubstValEquivA with (v:=v). auto. auto.
simpl. rewrite HsubstValEquivA with (v:=v). auto. auto. Qed.

Lemma substValEquivH: forall H s v E x, (HEval H s) = Some v -> Eval (SubstH E H x) s = Eval (SubstH E (hValToHExpr v) x) s.
intros. destruct E; simpl. erewrite AsubstValEquivH; auto.
erewrite BsubstValEquivH; auto.
erewrite HsubstValEquivH; auto.
Qed.

Lemma AsubstRes21A: forall E A s s' x v,
(AEval A s) = Some v -> s' = aUpdate s x (v) ->
(AEval (ASubstA (E) (A) (ASkalVar x)) s) = AEval (E) s'.
Proof.
intros.

induction E using AExpr_ind_mut with
(P:= fun H => (AEval A s) = Some v -> s' = aUpdate s x (v) ->
(HEval (HSubstA (H) (A) (ASkalVar x)) s) = HEval (H) s'); intros;
destruct s; destruct p; subst; auto.

intuition.
rewrite HsubstValEquivA with (v:=v) by auto.
rewrite AsubstValEquivA with (v:=v) in IHE2 by auto.
rewrite AsubstValEquivA with (v:=v) in IHE3 by auto.
rewrite HsubstValEquivA with (v:=v) in H3 by auto.
simpl in *.
destruct (AEval (ASubstA E1 (IntExpr v) (ASkalVar x)) (a, b, h0)).
destruct (AEval E1
         (fun y : ASkal =>
          if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b,
         h0)); inv IHE2.
destruct (AEval (ASubstA E2 (IntExpr v) (ASkalVar x)) (a, b, h0)).
destruct (AEval E2
         (fun y : ASkal =>
          if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b,
         h0)); inv IHE3.
destruct (HEval (HSubstA h (IntExpr v) (ASkalVar x)) (a, b, h0)).
destruct (HEval h
       (fun y : ASkal =>
        if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b, h0)); inv H3.
auto.
destruct (HEval h
    (fun y : ASkal =>
     if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b, h0)).
inv H3. auto.
destruct (AEval E2
    (fun y : ASkal =>
     if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b, h0)).
destruct (HEval h
    (fun y : ASkal =>
     if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b, h0)).
inv IHE3. auto. auto.
destruct (AEval E1
    (fun y : ASkal =>
     if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y, b, h0)
). inv IHE2. auto.

simpl. remember (beq_SkalVar (ASkalVar x) (ASkalVar a)). destruct b0. simpl. auto.
auto.

simpl in *. remember (AEval (ASubstA E1 A (ASkalVar x)) (a0,b,h)). destruct o.
remember (AEval (ASubstA E2 A (ASkalVar x)) (a0, b, h)). destruct o.
  remember (AEval E1
         (fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a0 y, b, h)).
destruct o.
remember (AEval E2 (fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a0 y, b, h)).
destruct o. inv IHE1. inv IHE2. auto. inv IHE2. inv IHE1.
remember (AEval E1
    (fun y : ASkal =>
     if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a0 y, b, h)).
destruct o. inv IHE1.
remember (AEval E2
    (fun y : ASkal =>
     if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a0 y, b, h)).
destruct o. inv IHE2. auto. auto. inv IHE2. inv IHE1.
auto.

simpl. rewrite IHE; auto. rewrite IHE0; auto.
Qed.

Lemma HsubstRes21A: forall E A s s' x v,
(AEval A s) = Some v -> s' = aUpdate s x (v) ->
(HEval (HSubstA (E) (A) (ASkalVar x)) s) = HEval (E) s'.
Proof.
intros.

induction E; intros;
destruct s; destruct p; subst; auto.

simpl in *.

repeat (erewrite AsubstRes21A; eauto). simpl.
destruct (HEval (HSubstA E A (ASkalVar x)) (a1, b, h)).
destruct (HEval E
        (fun y : ASkal =>
         if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a1 y, b,
        h)). inv IHE.
auto.
inv IHE.
destruct (HEval E
        (fun y : ASkal =>
         if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a1 y, b,
        h)).
inv IHE. auto.
Qed.

Lemma HsubstRes21H: forall E H s s' x v,
(HEval H s) = Some v -> s' = hUpdate s x v ->
(HEval (HSubstH E H (HSkalVar x)) s) = HEval E s'.
Proof.
intros.
induction E using HExpr_ind_mut with
(P0:= fun A =>
(AEval (ASubstH (A) (H) (HSkalVar x)) s) = AEval (A) s'); intros; subst.

destruct s; destruct p.
simpl. destruct (beq_SkalVar (HSkalVar x) (HSkalVar h)); auto.

auto.
simpl. rewrite IHE. rewrite IHE0. rewrite IHE1. auto.

simpl. destruct s; destruct p. simpl. auto.

auto.

simpl. rewrite IHE. rewrite IHE0. auto.

simpl. rewrite IHE. rewrite IHE0. auto.

Qed.

Lemma AsubstRes21H: forall E H s s' x v,
(HEval H s) = Some v -> s' = hUpdate s x (v) ->
(AEval (ASubstH (E) (H) (HSkalVar x)) s) = AEval (E) s'.
Proof.
intros. subst. induction E.

simpl. remember (fst (fst s) a). destruct o. destruct s. destruct p.
simpl in *. rewrite <- Heqo. auto.

destruct s. destruct p. simpl in *. rewrite <-Heqo. auto.

simpl in *. auto.

simpl.

rewrite <- IHE2.
rewrite <- IHE1. auto.

simpl. rewrite <- IHE.
erewrite HsubstRes21H. auto. apply H0.
auto.
Qed.

Lemma BsubstRes21H: forall E H s s' x v,
(HEval H s) = Some v -> s' = hUpdate s x v ->
(BEval (BSubstH E H (HSkalVar x)) s) = BEval E s'.
Proof.
intros. induction E; subst; auto; simpl.
destruct s; destruct p. auto. erewrite (AsubstRes21H a); eauto.
erewrite (AsubstRes21H a0); eauto.

rewrite IHE1. rewrite IHE2. auto.

rewrite IHE1. rewrite IHE2. auto.

rewrite IHE. auto.

Qed.

Lemma BsubstRes21A: forall E A s s' x v,
(AEval A s) = Some v -> s' = aUpdate s x (v) ->
(BEval (BSubstA ( E) (A) (ASkalVar x)) s) = BEval (E) s'.
Proof.
intros. subst. rewrite BsubstValEquivA with (v:=v) by auto. induction E.
simpl. remember (snd (fst s) b). destruct o. destruct s. destruct p. simpl. remember (b1 b).
destruct o. inv Heqo. rewrite <- H1 in Heqo0. inv Heqo0. auto. inv Heqo. rewrite <- H1 in Heqo0.
inv Heqo0.

destruct s. destruct p. simpl. remember (b0 b). destruct o. inv Heqo. rewrite <- Heqo0 in H1. inv H1. auto.

destruct s. destruct p. auto. destruct s. destruct p. simpl. rewrite (AsubstRes21A _ _ _ (((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a1 y), b0,h)) _ (v)).
rewrite (AsubstRes21A _ _ _ (((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a1 y), b0,h)) _ (v)). auto. auto. auto. auto. auto.

simpl. destruct s. destruct p.
remember ( BEval (BSubstA E1 (IntExpr v) (ASkalVar x)) (a, b,h)). destruct o. simpl in *.
remember ( BEval E1 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b,h)). destruct o.
remember (BEval (BSubstA E2 (IntExpr v) (ASkalVar x)) (a, b,h)). destruct o.
remember (BEval E2 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b,h)). destruct o.
inv IHE2. inv IHE1. auto. inv IHE2.
remember (BEval E2 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b,h)). destruct o.
inv IHE2. auto.
remember (BEval (BSubstA E2 (IntExpr v) (ASkalVar x)) (a, b,h)). destruct o.
remember (BEval E2 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y),b,h)). destruct o.
inv IHE1. inv IHE2. auto. simpl in *.
remember (BEval E1((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b,h)). destruct o.
inv IHE1. auto.

simpl. destruct s. destruct p. simpl in *.
remember ( BEval (BSubstA E1 (IntExpr v) (ASkalVar x)) (a, b,h)). destruct o.
remember ( BEval E1 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b, h)). destruct o.
remember (BEval (BSubstA E2 (IntExpr v) (ASkalVar x)) (a, b, h)). destruct o.
remember (BEval E2 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b, h)). destruct o.
inv IHE2. inv IHE1. auto. inv IHE2.
remember (BEval E2 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b, h)). destruct o.
inv IHE2. auto.
remember (BEval (BSubstA E2 (IntExpr v) (ASkalVar x)) (a, b, h)). destruct o.
remember (BEval E2 ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y),b, h)). destruct o.
inv IHE1. inv IHE2. auto.
remember (BEval E1((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b, h)). destruct o.
inv IHE1. auto.

simpl. destruct s. destruct p. simpl in *.
remember ( BEval (BSubstA E (IntExpr v) (ASkalVar x)) (a, b, h)). destruct o.
remember ( BEval E ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b, h)). destruct o.
inv IHE. auto. inv IHE.
remember (BEval E ((fun y : ASkal => if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else a y), b, h)). destruct o.
inv IHE. auto.
Qed.

Lemma substRes21A: forall E A s s' x v,
(AEval A s) = Some v -> s' = aUpdate s x (v) ->
(Eval (SubstA (E) (A) (ASkalVar x)) s) = Eval ( E) s'.
intros. destruct E. simpl. erewrite AsubstRes21A. Focus 2. apply H. Focus 2. apply H0.
auto. simpl. erewrite BsubstRes21A. Focus 2. apply H. Focus 2. apply H0. auto.
simpl. erewrite HsubstRes21A; eauto.
Qed.

Lemma substRes22A: forall A s x v s' E,
(AEval A s) = Some v -> s' = aUpdate s x (v) ->
(BEval (E) s' = Some (true) <-> ((Eval (SubstA (BExp E) (A) (ASkalVar x)) s) = Some (BValue true))).
Proof.
intros. split. intros. simpl. rewrite (BsubstRes21A _ _ _ s' _ v); auto. rewrite H1. auto.
intros. rewrite H0. simpl in H1. rewrite (BsubstRes21A _ _ _ s' _ v) in H1; auto. remember (BEval E s'). destruct o. inv H1. rewrite <- Heqo. auto.
inv H1.
Qed.

Lemma RemoveBSubstA: forall a s x v, AEval a (bUpdate s x (v)) = AEval a s.
intros. induction a using AExpr_ind_mut with
(P:=fun h => HEval h (bUpdate s x (v)) = HEval h s); destruct s; destruct p; auto.
simpl in *. rewrite IHa1. rewrite IHa2. rewrite IHa3. auto.
simpl in *. rewrite IHa1. rewrite IHa2. auto.
simpl in *. rewrite IHa0. rewrite IHa.
auto.
Qed.

Lemma RemoveBSubstH: forall a s x v, HEval a (bUpdate s x (v)) = HEval a s.
Proof.
intros. induction a; destruct s; destruct p; auto. simpl in *.
rewrite IHa. assert (R:=RemoveBSubstA a0 (a2,b,h)). simpl in R.
rewrite R. clear R. assert (R:=RemoveBSubstA a1 (a2,b,h)). simpl in R.
rewrite R. auto.
Qed.

Lemma substRes21H: forall E H s s' x v,
(HEval H s) = Some v -> s' = hUpdate s x (v) ->
(Eval (SubstH (E) (H) (HSkalVar x)) s) = Eval ( E) s'.
Proof.
intros. destruct E; simpl. erewrite AsubstRes21H; eauto.
erewrite BsubstRes21H; eauto.
erewrite HsubstRes21H; eauto.
Qed.

Lemma substRes22H: forall H s x v s' E,
(HEval H s) = Some v -> s' = hUpdate s x (v) ->
(BEval (E) s' = Some (true) <-> ((Eval (SubstH (BExp E) (H) (HSkalVar x)) s) = Some (BValue true))).
Proof.
intros. split; intros; subst; simpl in *. erewrite (BsubstRes21H E); eauto. rewrite H2. auto.
erewrite (BsubstRes21H) in H2; eauto. destruct (BEval E (hUpdate s x v)); inv H2; auto.
Qed.

Lemma BsubstRes21B: forall E B s s' x v,
(BEval B s) = Some v -> s' = bUpdate s x (v) ->
(BEval (BSubstB (E) (B) (BSkalVar x)) s) = BEval (E) s'.
Proof.
intros. subst. rewrite BsubstValEquivB with (v:=v).

induction E; intros.
simpl. destruct s. destruct p. simpl. remember (beq_SkalVar (BSkalVar x) (BSkalVar b)). destruct b1; auto.
auto.

unfold BSubstB. unfold BEval. rewrite RemoveBSubstA. rewrite RemoveBSubstA. auto.

simpl. rewrite IHE1. rewrite IHE2. auto.

simpl. rewrite IHE1. rewrite IHE2. auto.

simpl. rewrite IHE. auto.
auto.
Qed.

Lemma substRes22B: forall B s x v s' E,
(BEval B s) = Some v -> s' = bUpdate s x (v) ->
(BEval (E) s' = Some (true) <-> ((Eval (SubstB (BExp E) (B) (BSkalVar x)) s) = Some (BValue true))).
Proof.
intros. split. intros. simpl. rewrite (BsubstRes21B _ _ _ s' _ v); auto. rewrite H1. auto.
intros. rewrite H0. simpl in H1. rewrite (BsubstRes21B _ _ _ s' _ v) in H1; auto. remember (BEval E s'). destruct o. inv H1. rewrite <- Heqo. auto.
inv H1.
Qed.

Lemma substRes21B: forall E B s s' x v,
(BEval B s) = Some v -> s' = bUpdate s x (v) ->
(Eval (SubstB (E) (B) (BSkalVar x)) s) = Eval (E) s'.
intros. subst. destruct E. unfold Eval. erewrite RemoveBSubstA. simpl. auto.
unfold Eval. erewrite <- BsubstRes21B. Focus 2. apply H. Focus 2. auto. simpl. auto.
simpl. rewrite RemoveBSubstH. auto.
Qed.