proposition: Lemma cll_ill_soundness Γ A : ⟦Γ⟧ ⊢c [A]::∅ -> Γ ⊢i A \/ ill_has_bot A \/ exists f, In f Γ /\ ill_has_bot f.
proof: Proof. intros H. apply cll_ill_rec with (2 := eq_refl) in H. * rewrite ill_cll_ill_list, ill_cll_ill, <- ill_cll_has_bot_eq in H. destruct H as [ | [ | (f & G1 & G2) ] ]; auto. do 2 right. apply in_map_iff in G1. destruct G1 as (g & <- & ?). exists g; rewrite ill_cll_has_bot_eq; auto. * rewrite -> Forall_map with (f := ill_cll) (ll := A::Γ), Forall_forall. intros; apply ill_cll_from_ill. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL ill_cll)