(* RELOCATION N-STREAM ******************************************************)
-let rec apply (i: nat) on i: rtmap → nat ≝ ?.
+rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
* #n #f cases i -i
[ @n
| #i lapply (apply i f) -apply -i -f
(* Main inversion lemmas ****************************************************)
-lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 →
- j1 = j2 → f1 ≗ f2 → i1 = i2.
-/2 width=6 by at_inj/ qed-.
+theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2.
+/2 width=4 by at_inj/ qed-.