include "ground/relocation/gr_tl.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
(*** sle *)
coinductive gr_sle: relation gr_map ≝
"inclusion (generic relocation maps)"
'subseteq f1 f2 = (gr_sle f1 f2).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** sle_refl *)
corec lemma gr_sle_refl:
[ @(gr_sle_push … H H) | @(gr_sle_next … H H) ] -H //
qed.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** sle_inv_xp *)
lemma gr_sle_inv_push_dx:
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** sle_inv_pp *)
lemma gr_sle_inv_push_bi:
/3 width=3 by ex2_intro, or_introl, or_intror/
qed-.
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
(*** sle_px_tl *)
lemma gr_sle_push_sn_tl:
]
qed.
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
(*** sle_inv_tl_sn *)
lemma gr_sle_inv_tl_sn: