proposition: Fact fol_bin_sem_dec b A B : { A } + { ~ A } -> { B } + { ~ B } -> { fol_bin_sem b A B } + { ~ fol_bin_sem b A B }.
proof: Proof. revert b; intros [] HA HB; simpl; tauto. Qed.
imports: List Arith Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)