proposition: Lemma clos_aeq_wf_size : forall R, R << transp (ltof size) -> WF (clos_aeq R).
proof: Proof. intros R h. apply (WF_incl (transp (ltof size))). 2: apply transp_ltof_wf. intros t u tu. inversion tu; clear tu; subst. unfold transp, ltof. rewrite H, H0. apply h. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)