BiReplaceBi1Imp0 Show Code edit
## Substitution
##
## (<-> ph (-> [ ps ] ] ] th))
## (<-> [ ps ] [ ch ] )
## (<-> ph (-> [ [ [ ch ] th))
##
thm (BiReplaceBi1Imp0 () (
replacee (<-> ph (-> ps th))
substitution (<-> ps ch))
(<-> ph (-> ch th))
replacee substitution
(<-> ps ch)
th imbi1i
(<-> (-> ps th) (-> ch th))
bitri
(<-> ph (-> ch th))
)
edit