-
Amin Timany authored
commit 392b7b43 Author: Amin Timany <amintimany@gmail.com> Date: Tue May 3 21:25:10 2016 +0200 Finish using new iris with "proof mode" In Fμ and Fμ_ref we do support reduction under Fold. In fact `Unfold (Fold v)` is reduced to `v` if and only if v is a variable. commit 9825e341 Author: Amin Timany <amintimany@gmail.com> Date: Mon May 2 20:35:57 2016 +0200 Prove fundamental lemma of stlc is proven Change the Fμ to make the operational semantics reduce under Fold. Fundamental lemma for Fμ is partially proven (up to App).
f1ae6242