proposition: Lemma beq_term_true_iff u v : beq_term u v = true <-> u = v.
proof: Proof. unfold bool_of_rel. destruct (eq_term_dec u v); intuition. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)