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 "basic_2/dynamic/cnv_cpms_conf.ma".
17 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
19 (* Main preservation properties *********************************************)
21 (* Basic_2A1: uses: snv_preserve *)
22 lemma cnv_preserve (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] →
23 ∧∧ IH_cnv_cpms_conf_lpr a h G L T
24 & IH_cnv_cpm_trans_lpr a h G L T.
27 lapply (cnv_fwd_fsb … o … HT) -HT #H
28 @(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH
29 @conj [ letin aux ≝ cnv_cpms_conf_lpr_aux | letin aux ≝ cnv_cpm_trans_lpr_aux ]
30 @(aux … o … G L T) // #G0 #L0 #T0 #H
31 elim (IH … H) -IH -H //
34 theorem cnv_cpms_conf_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_conf_lpr a h G L T.
35 #a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=1 by/
38 (* Basic_2A1: uses: snv_cpr_lpr *)
39 theorem cnv_cpm_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpm_trans_lpr a h G L T.
40 #a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=2 by/
43 (* Advanced preservation properties *****************************************)
45 (* Basic_2A1: uses: snv_cprs_lpr *)
46 lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T.
47 #a #h #G #L1 #T1 #HT1 #n #T2 #H
48 @(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/