--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv".
+
+include "Lift/defs.ma".
+
+theorem lift_inv_sort_1: \forall l, i, h, x.
+ Lift l i (leaf (sort h)) x \to
+ x = leaf (sort h).
+ intros. inversion H; clear H; intros;
+ [ auto
+ | destruct H2
+ | destruct H3
+ | destruct H5
+ | destruct H5
+ ].
+qed.
+
+theorem lift_inv_lref_1: \forall l, i, j1, x.
+ Lift l i (leaf (lref j1)) x \to
+ (i > j1 \land x = leaf (lref j1)) \lor
+ (i <= j1 \land
+ \exists j2. (l + j1 == j2) \land x = leaf (lref j2)
+ ).
+ intros. inversion H; clear H; intros;
+ [ destruct H1
+ | destruct H2. clear H2. subst. auto
+ | destruct H3. clear H3. subst. auto depth = 5
+ | destruct H5
+ | destruct H5
+ ].
+qed.
+
+theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
+ Lift l i (intb r u1 t1) x \to
+ \exists u2, t2.
+ Lift l i u1 u2 \land
+ Lift l (succ i) t1 t2 \land
+ x = intb r u2 t2.
+ intros. inversion H; clear H; intros;
+ [ destruct H1
+ | destruct H2
+ | destruct H3
+ | destruct H5. clear H5 H1 H3. subst. auto depth = 5
+ | destruct H5
+ ].
+qed.
+
+theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
+ Lift l i (intf r u1 t1) x \to
+ \exists u2, t2.
+ Lift l i u1 u2 \land
+ Lift l i t1 t2 \land
+ x = intf r u2 t2.
+ intros. inversion H; clear H; intros;
+ [ destruct H1
+ | destruct H2
+ | destruct H3
+ | destruct H5
+ | destruct H5. clear H5 H1 H3. subst. auto depth = 5
+ ].
+qed.