(*
axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
                             ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
                             ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.

lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
                         ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
                         ∀n,T2.  ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
  elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
  [ #H #_ destruct //
  | #s #H #_ #_ #_ destruct //
  ]
| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
  elim (cnv_inv_bind … H0) #HV1 #_
  elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
  /3 width=6 by cnv_bind/
| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
  elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
  elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
  @(cnv_appl … Hm … HVW1)

(* Properties with restricted rt-transition for terms ***********************)

lemma pippo (a) (h) (o) (G) (L):
            ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
            ∀n1,T.  ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
            ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
            ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0
  elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
  [ #H1 #H2 destruct /2 width=4 by ex3_intro/
  | #s #H1 #H2 #H3 #Hs destruct
    elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
    /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
  ]
| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
  elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct
  elim (cpm_inv_bind1 … HX2) -HX2 *
  [ #V2 #T2 #HV12 #HT2 #H destruct
    elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
    @(ex3_intro … (ⓑ{p,I}V2.T0))
    [ /2 width=1 by cpm_bind/
    | 
    | /2 width=1 by tdeq_pair/

*)