proposition: Lemma pairInProofs: forall {A:Type} (l: list A) , list {a: A $ LIn a l}.
proof: Proof. induction l as [| a l Hind];[exact []|]. pose proof (map (pairInProofsCons l a) Hind) as Hind'. exact (exI(a,injL(eq_refl a))::Hind'). Defined.
imports: UsefulTypes bin_rels Omega