ndefinition bool_destruct_aux ≝
Πb1,b2:bool.ΠP:Prop.b1 = b2 →
- match b1 with
- [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
- | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
- ].
+ match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ].
ndefinition bool_destruct : bool_destruct_aux.
- #b1; #b2; #P;
+ #b1; #b2; #P; #H;
+ nrewrite < H;
nelim b1;
- nelim b2;
nnormalize;
- #H;
- ##[ ##2: napply False_ind;
- nchange with (match true with [ true ⇒ False | false ⇒ True]);
- nrewrite > H;
- nnormalize;
- napply I
- ##| ##3: napply False_ind;
- nchange with (match true with [ true ⇒ False | false ⇒ True]);
- nrewrite < H;
- nnormalize;
- napply I
- ##| ##1,4: napply (λx:P.x)
- ##]
+ napply (λx.x).
nqed.
nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
nelim x;
nelim y;
##[ ##1,4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H)
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
+ nnormalize; #H;
+ napply False_ind;
+ napply (bool_destruct … H)
##]
nqed.