fact: Definition binrel_list {T} (def : T) (R : @bin_rel T) (tls trs : list T) : [univ] := length tls = length trs # (forall (n : nat), n < length tls -> R (nth n tls def) (nth n trs def)).
imports: UsefulTypes bin_rels Omega