• Amin Timany's avatar
    Squashed commit of the following: · f1ae6242
    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).
fundamental.v 8.52 KB