proposition: Lemma extendFunrZEvalExact : forall (g : rNat -> bool) (n : rNat) (p : rZ) (s : bool), valRz p = n -> rZEval (extendFun n g s) p = match p with | rZPlus p => s | rZMinus _ => negb s end.
proof: Proof. intros g n p; case p; unfold extendFun in |- *; simpl in |- *; auto with stalmarck; intros r s H; case (rltDec r n); auto with stalmarck; rewrite H; intros; absurd (rlt n n); auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)