ImpReplaceBi1Ex1 Show Code edit
## Substitution
##
## (<-> ph (E. x [ ps ] ] ] ))
## (-> [ ps ] [ ch ] )
## (<-> ph (E. x [ [ [ ch ] ))
##
thm (ImpReplaceBi1Ex1 () (
replacee (<-> ph (E. x ps))
substitution (-> ps ch))
(-> ph (E. x ch))
replacee substitution
(-> ps ch)
x 19.22i
(-> (E. x ps) (E. x ch))
ImpReplaceBi1
(-> ph (E. x ch))
)
edit