2
Axiom Refl1 : forall x : nat, x = x.
3
Axiom Refl2 : forall x : nat, x = x.
4
Axiom Refl3 : forall x : nat, x = x.
10
Declare Module M: Sub.
16
Lemma Refl1 : forall x : nat, x = x.
19
Axiom Refl2 : forall x : nat, x = x.
20
Lemma Refl3 : forall x : nat, x = x.
36
Module B <: Main with Module M:=A.M := F A.M.
42
Lemma r1 : (A.M.Refl1 = B.M.Refl1).
47
Lemma r2 : (A.M.Refl2 = B.M.Refl2).
52
Lemma r3 : (A.M.Refl3 = B.M.Refl3).
57
Lemma t : (A.M.T = B.M.T).
62
Lemma a : (A.M.A = B.M.A).