orbi12i Show Code edit
## Infer the disjunction of two equivalences
thm (orbi12i () (1 (<-> p0 p1) 2 (<-> q0 q1)) (<-> (\/ p0 q0) (\/ p1 q1))
1 q0 orbi1i
(<-> (\/ p0 q0) (\/ p1 q0))
2 p1 orbi2i
(<-> (\/ p1 q0) (\/ p1 q1))
bitri
(<-> (\/ p0 q0) (\/ p1 q1))
)
edit