proposition: Lemma j_eq n (P : Pinf W) a (T' : Pinf W) (aP : mem a P) (naT : ~mem a T') (TP : T' [<=] P) X : j n aP naT TP X [=] add a X.
proof: Proof. destruct X as [X [XT cXn]]. refl. Qed.
imports: Coq(Morphisms Basics Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil DepChoice LogicUtil SetUtil FinSet InfSet NatUtil)