proposition: Lemma correctness_heyting : forall {n} (f1 f2 : @formula (Fin.t n)), poly_of_formula f1 = poly_of_formula f2 -> forall v, eval_formula (Vector.nth v) f1 = eval_formula (Vector.nth v) f2.
proof: Proof. intros n f1 f2 H v. assert (H1 := poly_of_formula_eval f1 v); assert (H2 := poly_of_formula_eval f2 v). remember (eval_formula (Vector.nth v) f1) as b1; remember (eval_formula (Vector.nth v) f2) as b2. rewrite H in H1; rewrite <- H1 in H2. destruct b1; destruct b2; simpl in *; (discriminate || auto). Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef