proposition: Lemma LTS_traceE t (T : LTS_trace t) : exists fl', LTS_init lts (fl' 0) /\ (forall i (LTi : NOmega.lt_nat_l i (trace_length t)) d, LTS_step lts (fl' i) (trace_nth i t d) (fl' (S i))).
proof: Proof. destruct t; ins; desf. exists fl'; split; ins. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription