X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_sor.ma;h=e76c1ca3c3bdd2f6f2656c709624597d1be417c6;hb=ebc170efe71cf4ee842acfbe58bb6864e76ba98c;hp=b93214beadafbf4198d5d64d27bda5c9009ede38;hpb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma index b93214bea..e76c1ca3c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -176,3 +176,17 @@ lemma sor_isfin: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∀f. f1 ⋓ f2 ≡ #f1 #f2 #Hf1 #Hf2 #f #Hf elim (sor_isfin_ex … Hf1 … Hf2) -Hf1 -Hf2 /3 width=6 by sor_mono, isfin_eq_repl_back/ qed-. + +(* Inversion lemmas on inclusion ********************************************) + +corec lemma sor_inv_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f1 ⊆ f. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 +/3 width=5 by sle_push, sle_next, sle_weak/ +qed-. + +corec lemma sor_inv_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⊆ f. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 +/3 width=5 by sle_push, sle_next, sle_weak/ +qed-.