fact: Fixpoint or (c1 c2:t) {struct c1} : t := match c1, c2 with | nil, _ => c2 | _, nil => c1 | l1::c1, l2::c2' => match compare l1 l2 with | Eq => l1 :: or c1 c2' | Lt => l1 :: or c1 c2 | Gt => l2 :: or_aux or l1 c1 c2' end end.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring