proposition: Lemma Pf_equiv_of_gen (P Q : Pf) P_val Q_val : P [=] P_val -> Q [=] Q_val -> P_val [=] Q_val -> P =f= Q.
proof: Proof. intros e1 e2. unfold Pf_equiv. rewrite e1, e2. auto. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)