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-.
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-.