# Module ...lib.coq.WhyExn

``` Implicit Arguments On. Section Generic. Variables U,T : Set. Inductive EM : Set := Val : T -> EM | Exn : U -> EM. Variables Q : U -> Prop. Variables P : T -> Prop. Definition qcomb : EM -> Prop       := [v]if v then P else Q. Inductive QEM [A:Set] : Set       := Qval : A -> (QEM A) | Qexn : (u:U)(Q u) -> (QEM A). Definition decomp : (v:EM)(qcomb v)->(QEM {t:T|(P t)}). Intros [t|u]; Simpl; Intro p. Apply Qval; Exists t; Trivial. Apply Qexn with u; Trivial. Defined. Definition uncurry : (A:Set;P:A->Prop;C:Set)((x:A)(P x)->C)->{x:A|(P x)}->C. Destruct 2; Intros. Apply H with x; Trivial. Defined. Definition QEM_mon : (A,B:Set)(A->B)->(QEM A)->(QEM B). Destruct 2; Intros. Apply Qval; Auto. Apply Qexn with u; Trivial. Defined. End Generic. Definition decomp1 [T:Set][P:T->Prop]                    [E1:Set][Q1:E1->Prop]                    [v:(EM E1 T); pv: (qcomb Q1 P v)]  : (QEM Q1 {t:T|(P t)})  := (decomp pv). Definition decomp2 [T:Set][P:T->Prop]                    [E1:Set][Q1:E1->Prop][E2:Set][Q2:E2->Prop]                    [v:(EM E1 (EM E2 T)); pv:(qcomb Q1 (qcomb Q2 P) v)]  : (QEM Q1 (QEM Q2 {t:T|(P t)}))  := (QEM_mon 2!Q1 (uncurry (!decomp1 T P E2 Q2)) (decomp pv)). Definition decomp3 [T:Set][P:T->Prop][E1:Set]                    [Q1:E1->Prop][E2:Set][Q2:E2->Prop][E3:Set][Q3:E3->Prop]                    [v:(EM E1 (EM E2 (EM E3 T)));                     pv:(qcomb Q1 (qcomb Q2 (qcomb Q3 P)) v)]   : (QEM Q1 (QEM Q2 (QEM Q3 {t:T|(P t)})))   := (QEM_mon 2!Q1 (uncurry (!decomp2 T P E2 Q2 E3 Q3)) (decomp pv)). Definition decomp4 [T:Set][P:T->Prop][E1:Set]                    [Q1:E1->Prop][E2:Set][Q2:E2->Prop]                    [E3:Set][Q3:E3->Prop][E4:Set][Q4:E4->Prop]                    [v:(EM E1 (EM E2 (EM E3 (EM E4 T))));                     pv:(qcomb Q1 (qcomb Q2 (qcomb Q3 (qcomb Q4 P))) v)]   : (QEM Q1 (QEM Q2 (QEM Q3 (QEM Q4 {t:T|(P t)}))) )   := (QEM_mon 2!Q1 (uncurry (!decomp3 T P E2 Q2 E3 Q3 E4 Q4)) (decomp pv)). ```

``` ```

Index
This page has been generated by coqdoc