fact: Definition BinRelExtension (X:Type) (A : X -> X -> Prop) : LRel X := fun ys => match ys with | nil => False | cons x xs => match xs with | nil => False | cons z zs => A x z end end.
imports: Coq(List) AlmostFull.PropBounded(AlmostFull)