BiReplaceBi1An1Bi1 Show Code edit
## Substitution
##
## (<-> ph (/\ ps (<-> ch [ th ] ] ] )))
## (<-> [ th ] [ ta ] )
## (<-> ph (/\ ps (<-> ch [ [ [ ta ] )))
##
thm (BiReplaceBi1An1Bi1 () (
replacee (<-> ph (/\ ps (<-> ch th)))
substitution (<-> th ta))
(<-> ph (/\ ps (<-> ch ta)))
replacee substitution
(<-> th ta)
ch bibi2i
(<-> (<-> ch th) (<-> ch ta))
BiReplaceBi1An1
(<-> ph (/\ ps (<-> ch ta)))
)
edit