proposition: Theorem inLt : forall (e : rExpr) (n : rNat), inRExpr n e -> rlt n (rnext (maxVar e)).
proof: Proof. simple induction e; intros. inversion H. inversion H. inversion H; simpl in |- *; auto with stalmarck. inversion H0; simpl in |- *; auto with stalmarck. inversion H1; simpl in |- *; auto with stalmarck. apply rltTransRnext1 with (m := maxVar r0); auto with stalmarck. apply rltTransRnext1 with (m := maxVar r1); auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)