proposition: Lemma l: forall T t, transport t T -> forall t', transport t' T.
proof: Proof. induction T; intuition auto; try lia. - Timeout 1 simp transport in *. intuition auto with *. Qed.
imports: TestSuite.issues.issue95_1 Lia Equations.Prop.Equations