X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FGRP511-1.ma;h=3817828bc213159c4d4229a7ee820e5b46adc4e5;hb=f6c887944d48d718f372a57f1609f3d059908aa8;hp=d25661700f94cae9766af45acb2b74b6b5b5607f;hpb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;p=helm.git diff --git a/helm/software/matita/contribs/ng_TPTP/GRP511-1.ma b/helm/software/matita/contribs/ng_TPTP/GRP511-1.ma index d25661700..3817828bc 100644 --- a/helm/software/matita/contribs/ng_TPTP/GRP511-1.ma +++ b/helm/software/matita/contribs/ng_TPTP/GRP511-1.ma @@ -44,25 +44,25 @@ include "logic/equality.ma". (* -------------------------------------------------------------------------- *) ntheorem prove_these_axioms_3: - ∀Univ:Type.∀A:Univ.∀B:Univ.∀C:Univ. + (∀Univ:Type.∀A:Univ.∀B:Univ.∀C:Univ. ∀a3:Univ. ∀b3:Univ. ∀c3:Univ. ∀inverse:∀_:Univ.Univ. ∀multiply:∀_:Univ.∀_:Univ.Univ. -∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply (multiply (multiply A B) C) (inverse (multiply A C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3)) +∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply (multiply (multiply A B) C) (inverse (multiply A C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))) . -#Univ. -#A. -#B. -#C. -#a3. -#b3. -#c3. -#inverse. -#multiply. -#H0. -nauto by H0; +#Univ ##. +#A ##. +#B ##. +#C ##. +#a3 ##. +#b3 ##. +#c3 ##. +#inverse ##. +#multiply ##. +#H0 ##. +nauto by H0 ##; nqed. (* -------------------------------------------------------------------------- *)