manual

[helm.git] / weblib / basics / logic.ma

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index b9dfed28c7d70dc1d39e7ca68fa9b5e533be02de..527e48429836af118c8f812430b6e2e95e6fe855 100644 (file)
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -269,4 +269,4 @@ qed.
 
 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[3].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
  #T #t #P #H #p >(\ 5a href="cic:/matita/basics/logic/lemmaK.def(2)"\ 6lemmaK\ 5/a\ 6 T t p) @H
-qed.
\ No newline at end of file
+qed.