Section Predicate_Calculus.
(* Ein einfaches Beispiel für Prädikatenlogik *)

Variable D:Set.
Variable R:D->D->Prop.

Section R_sym_trans.

Hypothesis R_symmetric: 
   forall x y:D, R x y -> R y x.
Hypothesis R_transitive: 
   forall x y z: D, R x y -> R y z -> R x z.

Lemma refl_if:
   forall x:D, (exists y, R x y) -> R x x.
Proof.
intro x.
intro x_Rlinked.
elim x_Rlinked.
intro y.
intro Rxy.
apply R_transitive with y.
assumption.
apply R_symmetric.
assumption.
Qed.

Print refl_if.
End R_sym_trans.

Print refl_if.
End Predicate_Calculus.

Section foo.
(* Ein weiteres einfaches Beispiel: *)

Variable f: nat->nat.
Hypothesis foo: f 0 = 0.
Lemma L1: forall k:nat, k=0 -> f k = k.
Proof.
intros k E.
rewrite E.
assumption.
Qed.
Print L1.

Hypothesis f10: f 1 = f 0.
Lemma L2: f(f 1) = 0.
Proof.
replace (f 1) with 0.
exact foo.
transitivity (f 0).
symmetry.
assumption.
symmetry.
assumption.
Qed.
Print L2.

End foo.