proposition: Fact bt_tc_incl_transitive s t : bt_transitive t -> s ⊆ t -> ↓s ⊆ t.
proof: Proof. intros H. induction s as [ | u Hu v Hv ]; simpl; auto. intros H1 x; btm simpl; rewrite bt_cup_spec. intros [ H2 | [ H2 | H2 ] ]. + rewrite H2; apply H1; btm simpl. + revert H2; apply Hu. intros a Ha; apply H with (1 := Ha), H1; btm simpl. + revert H2; apply Hv; intros ? ?; apply H1; btm simpl. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite seteq) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops)