BiReplaceImp0An1Al1Imp1 Show Code edit
## Substitution
##
## (-> (/\ ph (A. x (-> ps [ ch ] ] ] ))) ta)
## (<-> [ ch ] [ th ] )
## (-> (/\ ph (A. x (-> ps [ [ [ th ] ))) ta)
##
thm (BiReplaceImp0An1Al1Imp1 () (
replacee (-> (/\ ph (A. x (-> ps ch))) ta)
substitution (<-> ch th))
(-> (/\ ph (A. x (-> ps th))) ta)
replacee substitution
(<-> ch th)
ps imbi2i
(<-> (-> ps ch) (-> ps th))
BiReplaceImp0An1Al1
(-> (/\ ph (A. x (-> ps th))) ta)
)
edit