some restyling ...

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / aaa_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
index 15b4fe4e1d538af46c888fef18ea3755cf5b2936..bd1eb91a25d59b6a5db5dcf9929dee688f895e20 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
@@ -18,7 +18,7 @@ include "static_2/static/aaa.ma".
 
 (* Main inversion lemmas ****************************************************)
 
-theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
+theorem aaa_mono: ∀G,L,T,A1. ⦃G,L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G,L⦄ ⊢ T ⁝ A2 → A1 = A2.
 #G #L #T #A1 #H elim H -G -L -T -A1
 [ #G #L #s #A2 #H >(aaa_inv_sort … H) -H //
 | #I1 #G #L #V1 #B #_ #IH #A2 #H