1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fun".
17 include "Lift/inv.ma".
19 (* Functional properties ****************************************************)
21 theorem lift_total: \forall l, t, i. \exists u. Lift l i t u.
22 intros 2. elim t; clear t;
24 | lapply (nle_gt_or_le n i). decompose;
26 | lapply (nplus_total l n). decompose. auto
28 | lapply (H i1). lapply (H1 (succ i1)). decompose. auto
29 | lapply (H i1). lapply (H1 i1). decompose. auto
33 theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
34 \forall t2. Lift l i t t2 \to
36 intros 5. elim H; clear H i t t1;
37 [ lapply linear lift_inv_sort_1 to H1
38 | lapply linear lift_inv_lref_1_gt to H2, H1
39 | lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2
40 | lapply linear lift_inv_bind_1 to H5. decompose
41 | lapply linear lift_inv_flat_1 to H5. decompose
45 theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
46 \forall t2. Lift l i t2 t \to
48 intros 5. elim H; clear H i t1 t;
49 [ lapply linear lift_inv_sort_2 to H1
50 | lapply linear lift_inv_lref_2_gt to H2, H1
51 | lapply nle_nplus to H2 as H.
52 lapply linear nle_trans to H1, H as H0.
53 lapply lift_inv_lref_2_le_nplus to H3, H0, H2
54 | lapply linear lift_inv_bind_2 to H5. decompose
55 | lapply linear lift_inv_flat_2 to H5. decompose