proposition: Lemma lexd_incl : forall gt1 gt1', gt1 << gt1' -> forall gt2 gt2', (forall a, gt2 a << gt2' a) -> lexd gt1 gt2 << lexd gt1' gt2'.
proof: Proof. intros gt1 gt1' h1 gt2 gt2' h2 a a'. intro aa'. inversion aa'; subst. apply lexdl. apply h1. hyp. apply lexdr. apply h2. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)