qed-.
let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?.
* #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy
cases (after_inv_apply … Hx) -Hx #Hc #Hx
cases (after_inv_apply … Hy) -Hy #Hd
qed-.
let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?.
* #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy
cases (after_inv_apply … Hx) -Hx #Hc #Hx
cases (after_inv_apply … Hy) -Hy #Hd