• 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).
    f1ae6242
fundamental.v 11.7 KB