include "ground/notation/relations/predicate_u_1.ma".
include "ground/relocation/gr_isi.ma".
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
(*** isuni *)
inductive gr_isu: predicate gr_map ā
"uniformity condition (generic relocation maps)"
'PredicateU f = (gr_isu f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** isuni_inv_push *)
lemma gr_isu_inv_push (g): šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.
]
qed-.
-(* Basic forward lemmas *****************************************************)
+(* Basic destructions *******************************************************)
(*** isuni_fwd_push *)
lemma gr_isu_fwd_push (g): šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.