A formalization of \Beta-\eta equality in Coq using hereditary substitutions.
rodrigogribeiro / beta-eta-coq Goto Github PK
View Code? Open in Web Editor NEWFormalization and extraction of a decision procedure for beta-eta equality of simply typed lambda calculus in Coq