proposition: Lemma is_cnf_ff_inv : forall f1, is_cnf_ff f1 = true -> f1 = cnf_ff.
proof: Proof. unfold cnf_ff. intros f1 ; destruct f1 as [|c f1] ; simpl ; try congruence. destruct c ; simpl ; try congruence. destruct f1 ; try congruence. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid