proposition: Theorem gen_cell_sat: forall p s, valid_pos p -> (clause_sat (gen_cell p) s <-> In (get p s) ref_list).
proof: Proof. intros (x, y) s (H, H0); split; simpl. intros (((x1, y1), z1), (Hj1, Hj2)); simpl in Hj2. match goal with H: In ?l (gen_cell (Pos ?x ?y)) |- _ => case (gen_cell_correct l x y); auto; intros tmp _; case (tmp H); clear tmp H; auto end. intros z2 (Hz1, Hz2); injection Hz1. intros; subst; auto. intros H1. exists (L (Pos x y) (get (Pos x y) s)); split; auto. match goal with |- In ?l (gen_cell (Pos ?x ?y)) => case (gen_cell_correct l x y); auto; intros _ tmp; apply tmp; clear tmp end. exists (get (Pos x y) s); auto. red; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia