proposition: Lemma i_eq n P (Q : Pinf P) (U : Pinf Q) V (a : A) (VU_a : V [<=] rem a U) (aU : mem a U) (X : Pcard V n) : i aU VU_a X [=] add a X.
proof: Proof. refl. Qed.
imports: Coq(Morphisms Basics Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil DepChoice LogicUtil SetUtil FinSet InfSet NatUtil)