1 (* (C) 2014 Luca Bressan *)
5 definition power_one: ecl ≝
6 mk_ecl props (λz,z'. (z → z') ∧ (z' → z)) ?.
8 | #x #y * #h1 #h2 % [ @h2 | @h1 ]
9 | #x #y #z #h1 #h2 % cases h1 #hxy #hyx cases h2 #hyz #hzy
16 definition dpower_one: ∀I: ecl. edcl I.
21 [ #i1 #i2 #_ #y #y' #h @h
24 | #i1 #i2 #i3 #y #_ #_ @Rfl