# Library Continuations.weight.decl_exc

Inductive Txlev : Set :=
| xl1 : Txlev
| xl2 : Txlev.

Inductive Txval : TxlevSet :=
| xv1 : Txval xl1
| xv2 : boolTxval xl2.

Ltac AutoTx :=
intro l; elim l; simpl in |- *; intros v Hv; elim Hv; auto with v62.

Section inverse_of_xv2.

Theorem xl2_bool : Txval xl2bool.
intro x; elim x.
exact false.   intro b; exact b.
Defined.

Theorem l_xl2 : l : Txlev, l = xl2Txval lTxval xl2.
simple induction l.
intro E; discriminate E.
intros e v; exact v.
Defined.

Theorem inv_xv2_xl2_bool_aux :
(l : Txlev) (v : Txval l) (e : l = xl2),
l_xl2 l e v = xv2 (xl2_bool (l_xl2 l e v)).
simple induction v.
intros; absurd (xl1 = xl2); [ discriminate | assumption ].
auto with v62.
Qed.

Theorem inv_xv2_xl2_bool : v : Txval xl2, v = xv2 (xl2_bool v).
intro v.
cut (xl2 = xl2); [ intro e | auto with v62 ].
cut (l_xl2 xl2 e v = v); [ intro e'; elim e' | auto with v62 ].
apply inv_xv2_xl2_bool_aux.
Qed.

End inverse_of_xv2.

Theorem noteq_xv2_true_false : xv2 true = xv2 falseFalse.
intro E; discriminate E.
Qed.