• Amin Timany's avatar
    Change congruence lemmas of Fμ,ref,par · a17bf389
    Amin Timany authored
    The case of lam and case expressions that before required the terms to be
    well-typed now require terms to be closed.
    
    Separated definition context and context refinement from soundness_binary file.
    a17bf389
_CoqProject 856 Bytes