proposition: Lemma no_step_stack : forall s h e0, not (is_value e0) -> not (exists e0', step e0 e0') -> not (exists e1, step (apply_stack h s e0) e1).
proof: Proof. induction s; intros; try destruct a; simpl in *; auto. intros [e1 STEP]. assert (K1: not (exists e1', step (app e0 (apply_heap h (nom_to_exp n))) e1')). { intros [e1' SS]. inversion SS. subst. simpl in *. contradiction. subst. eauto. } assert (K2: not (is_value (app e0 (apply_heap h (nom_to_exp n))))). { simpl. auto. } pose (K := IHs h _ K2 K1). clearbody K. eauto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas