orbi1i Show Code edit
## Equivalence over Disjunction
##
## (<-> ph ] ] [ ps ] )
## (<-> (\/ ph ] ch) ] (\/ [ ps ] ch))
##
thm (orbi1i () (HEQ (<-> ph ps)) (<-> (\/ ph ch) (\/ ps ch))
ph ch orcom
(<-> (\/ ph ch) (\/ ch ph))
HEQ
(<-> ph ps)
ch orbi2i
(<-> (\/ ch ph) (\/ ch ps))
bitri
(<-> (\/ ph ch) (\/ ch ps))
ch ps orcom
(<-> (\/ ch ps) (\/ ps ch))
bitri
(<-> (\/ ph ch) (\/ ps ch))
)
edit