- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[helm.git] / helm / software / helena / matita / grundlagen_2.ma

diff --git a/helm/software/helena/matita/grundlagen_2.ma b/helm/software/helena/matita/grundlagen_2.ma
index 773c8a9deaa86aee61f85c4b06cb1ec16df53570..304439b026b5d06d8d87e54bcdd89d4a3ce4e388 100644 (file)
--- a/helm/software/helena/matita/grundlagen_2.ma
+++ b/helm/software/helena/matita/grundlagen_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* This file was generated by Helena 0.8.2 M (February 2015): do not edit *)
+(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****)
 
 include "basics/pts.ma".
 
@@ -584,13 +584,13 @@ definition l_orec3_th1 ≝ λa:Prop.λb:Prop.λc:Prop.λo:l_orec3 a b c.(l_orec3
 definition l_orec3_th2 ≝ λa:Prop.λb:Prop.λc:Prop.λo:l_orec3 a b c.(l_orec3i c a b (l_or3_th5 a b c (l_orec3e1 a b c o)) (l_ec3_th5 a b c (l_orec3e2 a b c o)) : l_orec3 c a b).
 
 (* constant 190 *)
-axiom l_e_is : Πsigma:Type[0].Πs:sigma.Πt:sigma.Prop.
+axiom l_e_is : ∀sigma:Type[0].∀s:sigma.∀t:sigma.Prop.
 
 (* constant 191 *)
-axiom l_e_refis : Πsigma:Type[0].Πs:sigma.l_e_is sigma s s.
+axiom l_e_refis : ∀sigma:Type[0].∀s:sigma.l_e_is sigma s s.
 
 (* constant 192 *)
-axiom l_e_isp : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.Πt:sigma.∀sp:p s.∀i:l_e_is sigma s t.p t.
+axiom l_e_isp : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀t:sigma.∀sp:p s.∀i:l_e_is sigma s t.p t.
 
 (* constant 193 *)
 definition l_e_symis ≝ λsigma:Type[0].λs:sigma.λt:sigma.λi:l_e_is sigma s t.(l_e_isp sigma (λx:sigma.l_e_is sigma x s) s t (l_e_refis sigma s) i : l_e_is sigma t s).
@@ -650,10 +650,10 @@ definition l_e_onee1 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma
 definition l_e_onee2 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma p.(l_ande2 (l_e_amone sigma p) (l_some sigma p) o1 : l_some sigma p).
 
 (* constant 212 *)
-axiom l_e_ind : Πsigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.sigma.
+axiom l_e_ind : Πsigma:Type[0].Πp:∀x:sigma.Prop.Πo1:l_e_one sigma p.sigma.
 
 (* constant 213 *)
-axiom l_e_oneax : Πsigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.p (l_e_ind sigma p o1).
+axiom l_e_oneax : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_one sigma p.p (l_e_ind sigma p o1).
 
 (* constant 214 *)
 definition l_e_one_th1 ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_one sigma p.λs:sigma.λsp:p s.(l_e_amonee sigma p (l_e_onee1 sigma p o1) (l_e_ind sigma p o1) s (l_e_oneax sigma p o1) sp : l_e_is sigma (l_e_ind sigma p o1) s).
@@ -788,25 +788,25 @@ definition l_e_bij_th1 ≝ λsigma:Type[0].λtau:Type[0].λupsilon:Type[0].λf:
 definition l_e_fise ≝ λsigma:Type[0].λtau:Type[0].λf:Πx:sigma.tau.λg:Πx:sigma.tau.λi:l_e_is (Πx:sigma.tau) f g.λs:sigma.(l_e_isp (Πx:sigma.tau) (λy:Πx:sigma.tau.l_e_is tau (f s) (y s)) f g (l_e_refis tau (f s)) i : l_e_is tau (f s) (g s)).
 
 (* constant 258 *)
-axiom l_e_fisi : Πsigma:Type[0].Πtau:Type[0].Πf:Πx:sigma.tau.Πg:Πx:sigma.tau.∀i:∀x:sigma.l_e_is tau (f x) (g x).l_e_is (Πx:sigma.tau) f g.
+axiom l_e_fisi : ∀sigma:Type[0].∀tau:Type[0].∀f:Πx:sigma.tau.∀g:Πx:sigma.tau.∀i:∀x:sigma.l_e_is tau (f x) (g x).l_e_is (Πx:sigma.tau) f g.
 
 (* constant 259 *)
 definition l_e_fis_th1 ≝ λsigma:Type[0].λtau:Type[0].λf:Πx:sigma.tau.λg:Πx:sigma.tau.λi:l_e_is (Πx:sigma.tau) f g.λs:sigma.λt:sigma.λj:l_e_is sigma s t.(l_e_tris tau (f s) (f t) (g t) (l_e_isf sigma tau f s t j) (l_e_fise sigma tau f g i t) : l_e_is tau (f s) (g t)).
 
 (* constant 260 *)
-axiom l_e_ot : Πsigma:Type[0].∀p:∀x:sigma.Prop.Type[0].
+axiom l_e_ot : Πsigma:Type[0].Πp:∀x:sigma.Prop.Type[0].
 
 (* constant 261 *)
-axiom l_e_in : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πo1:l_e_ot sigma p.sigma.
+axiom l_e_in : Πsigma:Type[0].Πp:∀x:sigma.Prop.Πo1:l_e_ot sigma p.sigma.
 
 (* constant 262 *)
-axiom l_e_inp : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πo1:l_e_ot sigma p.p (l_e_in sigma p o1).
+axiom l_e_inp : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀o1:l_e_ot sigma p.p (l_e_in sigma p o1).
 
 (* constant 263 *)
-axiom l_e_otax1 : Πsigma:Type[0].∀p:∀x:sigma.Prop.l_e_injective (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x).
+axiom l_e_otax1 : ∀sigma:Type[0].∀p:∀x:sigma.Prop.l_e_injective (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x).
 
 (* constant 264 *)
-axiom l_e_otax2 : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀sp:p s.l_e_image (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) s.
+axiom l_e_otax2 : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀sp:p s.l_e_image (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) s.
 
 (* constant 265 *)
 definition l_e_isini ≝ λsigma:Type[0].λp:∀x:sigma.Prop.λo1:l_e_ot sigma p.λo2:l_e_ot sigma p.λi:l_e_is (l_e_ot sigma p) o1 o2.(l_e_isf (l_e_ot sigma p) sigma (λx:l_e_ot sigma p.l_e_in sigma p x) o1 o2 i : l_e_is sigma (l_e_in sigma p o1) (l_e_in sigma p o2)).
@@ -842,19 +842,19 @@ axiom l_e_first : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.sigm
 axiom l_e_second : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.tau.
 
 (* constant 276 *)
-axiom l_e_pairis1 : Πsigma:Type[0].Πtau:Type[0].Πp1:l_e_pairtype sigma tau.l_e_is (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1.
+axiom l_e_pairis1 : ∀sigma:Type[0].∀tau:Type[0].∀p1:l_e_pairtype sigma tau.l_e_is (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1.
 
 (* constant 277 *)
 definition l_e_pairis2 ≝ λsigma:Type[0].λtau:Type[0].λp1:l_e_pairtype sigma tau.(l_e_symis (l_e_pairtype sigma tau) (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1)) p1 (l_e_pairis1 sigma tau p1) : l_e_is (l_e_pairtype sigma tau) p1 (l_e_pair sigma tau (l_e_first sigma tau p1) (l_e_second sigma tau p1))).
 
 (* constant 278 *)
-axiom l_e_firstis1 : Πsigma:Type[0].Πtau:Type[0].Πs:sigma.Πt:tau.l_e_is sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s.
+axiom l_e_firstis1 : ∀sigma:Type[0].∀tau:Type[0].∀s:sigma.∀t:tau.l_e_is sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s.
 
 (* constant 279 *)
 definition l_e_firstis2 ≝ λsigma:Type[0].λtau:Type[0].λs:sigma.λt:tau.(l_e_symis sigma (l_e_first sigma tau (l_e_pair sigma tau s t)) s (l_e_firstis1 sigma tau s t) : l_e_is sigma s (l_e_first sigma tau (l_e_pair sigma tau s t))).
 
 (* constant 280 *)
-axiom l_e_secondis1 : Πsigma:Type[0].Πtau:Type[0].Πs:sigma.Πt:tau.l_e_is tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t.
+axiom l_e_secondis1 : ∀sigma:Type[0].∀tau:Type[0].∀s:sigma.∀t:tau.l_e_is tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t.
 
 (* constant 281 *)
 definition l_e_secondis2 ≝ λsigma:Type[0].λtau:Type[0].λs:sigma.λt:tau.(l_e_symis tau (l_e_second sigma tau (l_e_pair sigma tau s t)) t (l_e_secondis1 sigma tau s t) : l_e_is tau t (l_e_second sigma tau (l_e_pair sigma tau s t))).
@@ -1208,16 +1208,16 @@ definition l_r_itef ≝ λa:Prop.λksi:Type[0].λx:Πt:a.ksi.λy:Πt:l_not a.ksi
 axiom l_e_st_set : Πsigma:Type[0].Type[0].
 
 (* constant 398 *)
-axiom l_e_st_esti : Πsigma:Type[0].Πs:sigma.Πs0:l_e_st_set sigma.Prop.
+axiom l_e_st_esti : ∀sigma:Type[0].∀s:sigma.∀s0:l_e_st_set sigma.Prop.
 
 (* constant 399 *)
-axiom l_e_st_setof : Πsigma:Type[0].∀p:∀x:sigma.Prop.l_e_st_set sigma.
+axiom l_e_st_setof : Πsigma:Type[0].Πp:∀x:sigma.Prop.l_e_st_set sigma.
 
 (* constant 400 *)
-axiom l_e_st_estii : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀sp:p s.l_e_st_esti sigma s (l_e_st_setof sigma p).
+axiom l_e_st_estii : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀sp:p s.l_e_st_esti sigma s (l_e_st_setof sigma p).
 
 (* constant 401 *)
-axiom l_e_st_estie : Πsigma:Type[0].∀p:∀x:sigma.Prop.Πs:sigma.∀e:l_e_st_esti sigma s (l_e_st_setof sigma p).p s.
+axiom l_e_st_estie : ∀sigma:Type[0].∀p:∀x:sigma.Prop.∀s:sigma.∀e:l_e_st_esti sigma s (l_e_st_setof sigma p).p s.
 
 (* constant 402 *)
 definition l_e_st_empty ≝ λsigma:Type[0].λs0:l_e_st_set sigma.(l_none sigma (λx:sigma.l_e_st_esti sigma x s0) : Prop).
@@ -1286,7 +1286,7 @@ definition l_e_st_isset_th1 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_s
 definition l_e_st_isset_th2 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_st_set sigma.λi:l_e_is (l_e_st_set sigma) s0 t0.(λx:sigma.λy:l_e_st_esti sigma x t0.l_e_st_issete2 sigma s0 t0 i x y : l_e_st_incl sigma t0 s0).
 
 (* constant 424 *)
-axiom l_e_st_isseti : Πsigma:Type[0].Πs0:l_e_st_set sigma.Πt0:l_e_st_set sigma.∀i:l_e_st_incl sigma s0 t0.∀j:l_e_st_incl sigma t0 s0.l_e_is (l_e_st_set sigma) s0 t0.
+axiom l_e_st_isseti : ∀sigma:Type[0].∀s0:l_e_st_set sigma.∀t0:l_e_st_set sigma.∀i:l_e_st_incl sigma s0 t0.∀j:l_e_st_incl sigma t0 s0.l_e_is (l_e_st_set sigma) s0 t0.
 
 (* constant 425 *)
 definition l_e_st_isset_th3 ≝ λsigma:Type[0].λs0:l_e_st_set sigma.λt0:l_e_st_set sigma.λs:sigma.λses0:l_e_st_esti sigma s s0.λn:l_not (l_e_st_esti sigma s t0).(l_imp_th3 (l_e_is (l_e_st_set sigma) s0 t0) (l_e_st_esti sigma s t0) n (λt:l_e_is (l_e_st_set sigma) s0 t0.l_e_st_issete1 sigma s0 t0 t s ses0) : l_not (l_e_is (l_e_st_set sigma) s0 t0)).