(* Properties with fold for restricted closures *****************************)
lemma vpushs_fold (M): is_model M → is_extensional M →
- ∀L,T1,T2,gv,lv.
- (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) →
- ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv].
+ ∀L,T1,T2,gv,lv.
+ (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) →
+ ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv].
#M #H1M #H2M #L elim L -L [| #K * [| * ]]
[ #T1 #T2 #gv #lv #H12
>fold_atom >fold_atom
>fold_pair >fold_pair
@IH -IH #v #Hv
@(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ]
- /4 width=1 by vpushs_abbr, mr/
+ /4 width=1 by vpushs_abbr, mc, mr/
| #W #IH #T1 #T2 #gv #lv #H12
>fold_pair >fold_pair
/5 width=1 by vpushs_abst, mx, mr/
(* Inversion lemmas with fold for restricted closures ***********************)
-lemma vpushs_inv_fold (M): is_model M →
- ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] →
- ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v].
-#M #HM #L elim L -L [| #K * [| * ]]
+lemma vpushs_inv_fold (M): is_model M → is_injective M →
+ ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] →
+ ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v].
+#M #H1M #H2M #L elim L -L [| #K * [| * ]]
[ #T1 #T2 #gv #lv
>fold_atom >fold_atom #H12 #v #H
lapply (vpushs_inv_atom … H) -H // #Hv
>fold_pair >fold_pair #H12 #y #H
elim (vpushs_inv_abbr … H) -H // #v #Hlv #Hv
lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12
- /4 width=7 by ti_comp, veq_refl, md, mq/
+ @(mq … H1M) [4,5: @(ti_comp … Hv) /3 width=2 by veq_refl/ |1,2: skip ]
+ /4 width=7 by ti_comp, ti_fwd_abbr_dx, veq_refl, mq/
| #W #IH #T1 #T2 #gv #lv
>fold_pair >fold_pair #H12 #y #H
elim (vpushs_inv_abst … H) -H // #v #d #Hlv #Hv