include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
(*** sor_tls *)
lemma gr_sor_tls:
∀f1,f2,f. f1 ⋓ f2 ≘ f →
- â\88\80n. ⫱*[n]f1 â\8b\93 ⫱*[n]f2 â\89\98 ⫱*[n]f.
+ â\88\80n. â«°*[n]f1 â\8b\93 â«°*[n]f2 â\89\98 â«°*[n]f.
#f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n
/2 width=1 by gr_sor_tl/
qed.