-ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##1: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##2: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##3: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##4: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##5: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##6: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##7: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##8: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##9: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##10: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##11: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##12: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##13: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##14: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##15: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-
-ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
- #e2; #P; ncases e2; nnormalize; #H;
- ##[ ##16: napply (λx:P.x)
- ##| ##*: napply False_ind;
- nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
- nrewrite > H; nnormalize; napply I
- ##]
-nqed.
-