include "ground/relocation/tr_pap_pat.ma".
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
(* Main inversions **********************************************************)
(*** apply_inj *)
theorem tr_pap_inj (f):
- ∀i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+ ∀i1,i2,j. f@⧣❨i1❩ = j → f@⧣❨i2❩ = j → i1 = i2.
/2 width=4 by pr_pat_inj/ qed-.