proposition: Theorem clause_insert_valid: forall c cs s, valid_clause c s -> valid cs s -> valid (clause_insert c cs) s.
proof: Proof. intros c cs s H H1 n1 c1 Hc1. case (clause_insert_in (n1, c1) c cs); auto. intros tmp _; case tmp; clear tmp; auto; intros H2. injection H2; intros; subst; auto. apply (H1 n1 c1); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia