proposition: Lemma eqApp s s' u u' : s == s' -> u == u' -> app s u == app s' u'.
proof: Proof. Proof with eauto using equiv, step. intros H; revert u u'; induction H; intros z z' H'... - eapply eqTrans. eapply eqStep. eapply stepAppL. eassumption. induction H'... - induction H'... Qed.
imports: Lia