HERMIT.Dictionary.Reasoning
externals
data CoreExprEquality
data RewriteCoreExprEqualityBox
data TransformCoreExprEqualityStringBox
type CoreExprEqualityProof c m
flipCoreExprEquality
eqLhsIntroR
eqRhsIntroR
birewrite
extensionalityR
CoreExprEquality
lhsT
rhsT
bothT
forallVarsT
lhsR
rhsR
bothR
ppCoreExprEqualityT
proveCoreExprEqualityT
verifyCoreExprEqualityT
verifyEqualityLeftToRightT
verifyEqualityCommonTargetT
verifyIsomorphismT
verifyRetractionT
retractionBR
alphaEqualityR
unshadowEqualityR
instantiateDictsR
instantiateEquality
instantiateEqualityVar
instantiateEqualityVarR
discardUniVars