proposition: Theorem rel_dec_neq_false : forall x y, ~eqt x y -> rel_dec x y = false.
proof: Proof. intros. remember (x ?[ eqt ] y). symmetry in Heqb. destruct b; try reflexivity. exfalso. eapply (@rel_dec_correct _ _ _ rc) in Heqb. auto. Qed.
imports: Coq.Bool.Bool Coq.Classes.RelationClasses