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 include "ground/relocation/gr_pat_id.ma".
16 include "ground/relocation/gr_pat_pat.ma".
18 (* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
20 (* Advanced Forward lemmas on id ********************************************)
23 lemma gr_pat_id_des (i1) (i2):
24 @❪i1,𝐢❫ ≘ i2 → i1 = i2.
25 /2 width=4 by gr_pat_mono/ qed-.
27 (* Main properties on id ****************************************************)
30 theorem gr_pat_div_id_dx (f):
33 lapply (gr_pat_id_des … H0) -H0 #H destruct
34 /2 width=3 by ex2_intro/
38 theorem gr_pat_div_id_sn (f):
40 /3 width=6 by gr_pat_div_id_dx, gr_pat_div_comm/ qed-.