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/LOGIC/Insert/fun".
17 include "CLE/defs.ma".
18 include "Insert/inv.ma".
20 (* Functional properties ****************************************************)
22 theorem insert_total: \forall S,i,P. i <= P \to \exists Q. Insert S i P Q.
23 intros 4; elim H; clear H i P;
27 theorem insert_inj: \forall S1,i,P, Q. Insert S1 i P Q \to
28 \forall S2. Insert S2 i P Q \to S1 = S2.
29 intros 5; elim H; clear H i P Q;
30 [ lapply linear insert_inv_zero to H1; destruct; autobatch
31 | lapply linear insert_inv_succ to H3; decompose; destruct; autobatch