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