proposition: Fact cll_ill_cll f : from_ill f -> [⟨f⟩] = f.
proof: Proof. induction f as [ | [] | [] | [] ]; simpl; try tauto; intros; f_equal; tauto. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL)