orbi2i Show Code edit
## Equivalence over Disjunction
##
## (<-> [ ph ] [ [ ps)
## (<-> (\/ ch [ ph ] ) [ (\/ ch [ ps))
##
thm (orbi2i () (HEQ (<-> ph ps)) (<-> (\/ ch ph) (\/ ch ps))
ch ph df-or
(<-> (\/ ch ph) (-> (-. ch) ph))
HEQ
(<-> ph ps)
(-. ch) imbi2i
(<-> (-> (-. ch) ph) (-> (-. ch) ps))
bitri
(<-> (\/ ch ph) (-> (-. ch) ps))
ch ps df-or
(<-> (\/ ch ps) (-> (-. ch) ps))
bicomi
(<-> (-> (-. ch) ps) (\/ ch ps))
bitri
(<-> (\/ ch ph) (\/ ch ps))
)
edit