Step
*
of Lemma
trivial-record-update
∀[r,z:Top]. (r[z := r.z] ~ λx.if x =a z then r x else r x fi )
BY
{ ((UnivCD THENA Auto)
THEN RW (BasicSymbolicComputeC []) 0
THEN EqCD
THEN RenameVar `a' (-1)
THEN (InstLemma `atom_eq_sq_normalize` [⌜λ2z.r z⌝;⌜r a⌝;⌜a⌝;⌜z⌝]⋅ THENA Auto)
THEN RevHypSubst (-1) 0⋅
THEN Auto) }
Latex:
Latex:
\mforall{}[r,z:Top]. (r[z := r.z] \msim{} \mlambda{}x.if x =a z then r x else r x fi )
By
Latex:
((UnivCD THENA Auto)
THEN RW (BasicSymbolicComputeC []) 0
THEN EqCD
THEN RenameVar `a' (-1)
THEN (InstLemma `atom\_eq\_sq\_normalize` [\mkleeneopen{}\mlambda{}\msubtwo{}z.r z\mkleeneclose{};\mkleeneopen{}r a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{} THENA Auto)
THEN RevHypSubst (-1) 0\mcdot{}
THEN Auto)
Home
Index