Administrative commit restoring the repository to the usual shape.

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 5e97f9b5c1bdd4b27da7613edad60fa8c644b917..c64f887c6fe0f6b36d90dfebb5a7f2c61897f59e 100644 (file)
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -223,5 +223,4 @@ definition R4 :
 qed.
 
 (* TODO concrete definition by means of proof irrelevance *)
-axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
-
+axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
\ No newline at end of file

diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma
index 3081fa96b05d8d5a3c966372a9b609b243afcf34..34d6fe11cd9b9bae04e91bb48aeddce65f554982 100644 (file)
--- a/weblib/basics/relations.ma
+++ b/weblib/basics/relations.ma
@@ -102,4 +102,4 @@ notation " f \eqF g " non associative with precedence 45
 for @{'eqF ? ? f g}.
 
 interpretation "functional extentional equality" 
-'eqF A B f g = (exteqF A B f g).
\ No newline at end of file
+'eqF A B f g = (exteqF A B f g).

diff --git a/weblib/ricciott4/prova.ma b/weblib/ricciott4/prova.ma
deleted file mode 100644 (file)
index 9ca5a7e..0000000
--- a/weblib/ricciott4/prova.ma
+++ /dev/null
@@ -1 +0,0 @@
-axiom paperino : Prop.
\ No newline at end of file