proposition: Lemma LTS_complete_trace_weaken t : LTS_complete_trace t -> LTS_trace t.
proof: Proof. destruct t; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription