Lemma foo_aplus_left: forall a1 a2 n1, aeval_small_closed a1 (ANum n1) -> aeval_small_closed (APlus a1 a2) (APlus (ANum n1) a2).
Proof.
  intros a1 a2 n1 H. induction H.
    apply AE_closed_step. apply AEPlus_cong_left. apply H.
    apply AE_closed_refl.
    apply AE_closed_trans with  (a2:=APlus a0 a2).
      apply IHaeval_small_closed1.
      apply IHaeval_small_closed2.
Qed.

Lemma foo_aplus_right: forall a1 a2 n2, aeval_small_closed a2 (ANum n2) -> aeval_small_closed (APlus a1 a2) (APlus a1 (ANum n2)).
Proof.
  intros a1 a2 n2 H. induction H.
    apply AE_closed_step. apply AEPlus_cong_right. apply H.
    apply AE_closed_refl.
    apply AE_closed_trans with  (a2:=APlus a1 a2).
      apply IHaeval_small_closed1.
      apply IHaeval_small_closed2.
Qed.



Lemma foo_AEIf0_cong_left : forall a1 a1' a2 a3,
    aeval_small_closed a1 a1' -> aeval_small_closed (AIf0 a1 a2 a3) (AIf0 a1' a2 a3).
Proof.
  intros. induction H. 
    apply AE_closed_step. apply AEIf0_cong_left. apply H.
    apply AE_closed_refl. 
    apply AE_closed_trans with (a2:=AIf0 a0 a2 a3).
      apply IHaeval_small_closed1.       apply IHaeval_small_closed2.
Qed.

(* CMSC 631 *)
Lemma aeval_big_small : forall a n,
  aeval_big a n -> aeval_small_closed a (ANum n).
Proof.
  intros. induction H.
    apply AE_closed_refl.
      apply AE_closed_trans with  (a2:=APlus (ANum n1) (ANum n2)).
        apply AE_closed_trans with  (a2:=APlus (ANum n1) a2).
          apply foo_aplus_left. apply IHaeval_big1.
          apply foo_aplus_right. apply IHaeval_big2.
        apply AE_closed_step. apply AEPlus.
      apply AE_closed_trans with  (a2:= AIf0 (ANum 0) a2 a3).
        apply foo_AEIf0_cong_left. apply IHaeval_big1. apply AE_closed_trans with  (a2:= a2).
          apply AE_closed_step. apply AEIF0_True.
          apply IHaeval_big2.
      apply AE_closed_trans with  (a2:= AIf0 (ANum n1) a2 a3).
        apply foo_AEIf0_cong_left. apply IHaeval_big1. apply AE_closed_trans with  (a2:= a3).
          apply AE_closed_step. apply AEIF0_False. apply H0.
          apply IHaeval_big2.
Qed.