matita/matita/contribs/mf/power_one.ma

   1 (* (C) 2014 Luca Bressan *)
   2
   3 include "model.ma".
   4
   5 definition power_one: ecl ≝
   6  mk_ecl props (λz,z'. (z → z') ∧ (z' → z)) ?.
   7  % [ #x % #h @h
   8    | #x #y * #h1 #h2 % [ @h2 | @h1 ]
   9    | #x #y #z #h1 #h2 % cases h1 #hxy #hyx cases h2 #hyz #hzy
  10      [ #hx @(hyz (hxy hx))
  11      | #hz @(hyx (hzy hz))
  12      ]
  13    ]
  14 qed.
  15
  16 definition dpower_one: ∀I: ecl. edcl I.
  17  #I %
  18  [ #i @power_one
  19  | #i1 #i2 #e #p @p
  20  | %
  21    [ #i1 #i2 #_ #y #y' #h @h
  22    | #i1 #i2 #_ #_ @Rfl
  23    | #i @Rfl
  24    | #i1 #i2 #i3 #y #_ #_ @Rfl
  25    ]
  26  ]
  27 qed.
  28