proposition: Lemma binrel_list_cons : forall {T : Type} R (def a b :T ) ta tb, (binrel_list def R ta tb # R a b) <=> (binrel_list def R (a::ta) (b :: tb)).
proof: Proof. split; introv hyp; unfold binrel_list in hyp; unfold binrel_list. - repnd. simpl. dands;spcf;[]. introv Hlt. destruct n; spc. dimp (hyp0 n); spc; omega. - allsimpl. repnd. dands ;spcf. + introv Hlt. dimp (hyp (S n));sp; omega. + dimp (hyp 0); spc; omega. Qed.
imports: UsefulTypes bin_rels Omega