proposition: Theorem length_clause_insert: forall c cs, length (clause_insert c cs) = S (length cs).
proof: Proof. intros c cs; unfold clause_insert; apply ocons_length. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia