proposition: Lemma eva_Sn_n n s : eva (S n) s = None -> eva n s = None.
proof: Proof. intros H; destruct s, n; try reflexivity; try now inv H. simpl. destruct (eva n s1) eqn:Hs1, (eva n s2) eqn:Hs2. - destruct t; try reflexivity. assert (Hs' : eva (S n) s1 = Some (lam t)) by eauto using eva_n_Sn. assert (Ht' : eva (S n) s2 = Some (t0)) by eauto using eva_n_Sn. destruct (eva n (subst t 0 t0)) eqn:Ht; try reflexivity. assert (H' : eva (S n) (subst t 0 t0) = Some t1) by eauto using eva_n_Sn. rewrite <- H. change (Some t1 = match eva (S n) s1, eva (S n) s2 with | Some (lam s), Some t => eva (S n) (subst s 0 t) | _ , _ => None end). rewrite Hs', Ht'. rewrite H'. reflexivity. - destruct t; reflexivity. - reflexivity. - reflexivity. Qed.
imports: Coq.Logic.ConstructiveEpsilon