proposition: Lemma beq_term_refl u : beq_term u u = true.
proof: Proof. unfold bool_of_rel. destruct (eq_term_dec u u). refl. cong. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)