proposition: Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
proof: Proof. induction p;destruct q;simpl;clean. - intro h;generalize (pos_eq_refl _ _ h);congruence. - case_eq (form_eq p1 q1);clean. intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. - case_eq (form_eq p1 q1);clean. intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. - case_eq (form_eq p1 q1);clean. intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. Qed.
imports: List Bintree Bool BinPos