matita/matita/contribs/mf/power.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4
   5 definition fun_to_power_one: est → ecl ≝
   6  λB. mk_ecl
   7  (Σh: fun_to_props B. ∀y1,y2: B. eq … y1 y2 → (conj (h y1 → h y2) (h y2 → h y1)))
   8  (λz,z'. ∀y: B. conj ((Sig1 … z) y → (Sig1 … z') y)
   9                          (implies ((Sig1 … z') y) ((Sig1 … z) y)))
  10  ?.
  11  % [ #x #y % #h @h
  12    | #x #x' #h #b % #k cases (h b) [ #_ #r | #r #_ ] @(r k)
  13    | #x #x' #x'' #h1 #h2 #b cases (h1 b) #k10 #k01 cases (h2 b) #k21 #k12 %
  14      #r [ @(k21 (k10 r)) | @(k01 (k12 r)) ]
  15    ]
  16 qed.
  17