proposition: Theorem soundness {Γ τ} {e : Exp Γ τ} {v} {se} : e ---> v → SemExp e se = SemExp v se.
proof: Proof. intros. induction H; simpl; auto. - now rewrite IHStep. - now rewrite IHStep. - now rewrite IHStep. - now rewrite IHStep. - rewrite <- SemExp_SubSem. f_equal; simpl. simp SubSem. now rewrite SubSem_idSub. - now rewrite IHStep. - now rewrite IHStep. Qed.
imports: Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Log Category.Instance.Lambda.Sub Category.Instance.Lambda.Sem Category.Instance.Lambda.Step Equations(Equations)