X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Fmf%2Fpower.ma;fp=matita%2Fmatita%2Fcontribs%2Fmf%2Fpower.ma;h=27a84ec3b5d6c53abc09a41bda7c692cff3c3476;hb=b3aa03ebf904d8c7290aa44b4ce80bf3f976fb2e;hp=0000000000000000000000000000000000000000;hpb=e83cd27fc0694c34baf35c8b80d32317e51be707;p=helm.git

diff --git a/matita/matita/contribs/mf/power.ma b/matita/matita/contribs/mf/power.ma
new file mode 100644
index 000000000..27a84ec3b
--- /dev/null
+++ b/matita/matita/contribs/mf/power.ma
@@ -0,0 +1,17 @@
+(* (C) 2014 Luca Bressan *)
+
+include "model.ma".
+
+definition fun_to_power_one: est → ecl ≝ 
+ λB. mk_ecl
+ (Σh: fun_to_props B. ∀y1,y2: B. eq … y1 y2 → (conj (h y1 → h y2) (h y2 → h y1)))
+ (λz,z'. ∀y: B. conj ((Sig1 … z) y → (Sig1 … z') y)
+                         (implies ((Sig1 … z') y) ((Sig1 … z) y)))
+ ?.
+ % [ #x #y % #h @h 
+   | #x #x' #h #b % #k cases (h b) [ #_ #r | #r #_ ] @(r k) 
+   | #x #x' #x'' #h1 #h2 #b cases (h1 b) #k10 #k01 cases (h2 b) #k21 #k12 %
+     #r [ @(k21 (k10 r)) | @(k01 (k12 r)) ]
+   ]
+qed.
+