proposition: Lemma computesExt X (tt : TT X) (x x' : X) s: extEq x x' -> computes tt x s -> computes tt x' s.
proof: Proof. induction tt in x,x',s |-*;intros eq. - inv eq. tauto. - cbn in eq|-*. intros [H1 H2]. split. 1:tauto. intros y t exts. specialize (H2 y t exts) as (v&R&H2). exists v. split. 1:assumption. eapply IHtt2. 2:now eassumption. apply eq. Qed.
imports: String