proposition: Lemma le_binrel_list_un : forall {T:Type} (def : T) (R: @bin_rel T) (Rul Rur: T -> [univ]), le_bin_rel R (indep_bin_rel Rul Rur) -> forall (la lb : list T), binrel_list def R la lb -> (forall x:T , LIn x la -> Rul x) # (forall x:T , LIn x lb -> Rur x).
proof: Proof. introv Hle Hb. repnud Hle. repnud Hb. unfold indep_bin_rel in Hle. split; introv Hin; apply in_nth3 with (def:=def) in Hin; exrepnd; subst; dimp (Hb n); spc; apply Hle in hyp; sp. Qed.
imports: UsefulTypes bin_rels Omega