proposition: Lemma equalBeforeExtend : forall (g : rNat -> bool) (n m : rNat) (s : bool), rlt n (rnext m) -> equalBefore n g (extendFun m g s).
proof: Proof. intros g n m s H; simpl in |- *; auto with stalmarck. red in |- *; auto with stalmarck. intros p H'; unfold extendFun in |- *; case (rltDec p m); auto with stalmarck. intros s0; case s0; auto with stalmarck. intros H'0; absurd (rlt (rnext m) n); auto with stalmarck. apply rltAntiSym; auto with stalmarck. apply rltTransRnext1 with (m := p); auto with stalmarck. intros H'0; rewrite <- H'0 in H. case (rNextInv n p); auto with stalmarck. intros H'1; absurd (p = n); auto with stalmarck. apply rltDef2; auto with stalmarck. intros H'1; absurd (rlt n p); auto with stalmarck. apply rltAntiSym; auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)