proposition: Theorem G_eill_sound Σ Γ p : Σ; Γ ⊦ p -> map (fun c => !⦑c⦒) Σ ++ map £ Γ ⊢ £ p.
proof: Proof. revert Σ; intros Si. induction 1 as [ u | Ga De p H1 H2 IH2 | Ga a p q H1 H2 IH2 | Ga De p q r H1 H2 IH2 H3 IH3 | Ga p q r H1 H2 IH2 H3 IH3 ]. + rewrite <- map_map; apply S_ill_restr_weak; apply in_ill1_ax. + revert IH2; apply in_ill1_perm. apply Permutation_app; auto. apply Permutation_map; auto. + rewrite <- map_map; apply S_ill_restr_weak_cntr with (1 := in_map _ _ _ H1); simpl. rewrite map_map. apply in_ill1_bang_l. apply in_ill1_perm with (((£ a ⊸ £ p) ⊸ £ q) :: ((map (fun c => !⦑c⦒) Si ++ map £ Ga) ++ nil)). * rewrite app_nil_r; auto. * apply in_ill1_limp_l. 2: apply in_ill1_ax. apply in_ill1_limp_r. revert IH2; apply in_ill1_perm. simpl; apply Permutation_sym, Permutation_cons_app; auto. + rewrite <- map_map. apply S_ill_restr_cntr. rewrite map_map. rewrite <- map_map; apply S_ill_restr_weak_cntr with (1 := in_map _ _ _ H1); simpl; rewrite map_map. apply in_ill1_bang_l. rewrite map_app. apply in_ill1_perm with (£ p ⊸ £ q ⊸ £ r :: (map (fun c => !⦑c⦒) Si ++ map £ Ga) ++ (map (fun c => !⦑c⦒) Si ++ map £ De)). * apply Permutation_cons; auto. rewrite <- app_assoc; apply Permutation_app; auto. do 2 rewrite app_assoc; apply Permutation_app; auto. apply Permutation_app_comm. * apply in_ill1_limp_l; auto. apply in_ill1_perm with (£ q ⊸ £ r :: ((map (fun c => !⦑c⦒) Si ++ map £ De) ++ nil)). - rewrite app_nil_r; auto. - apply in_ill1_limp_l; auto. apply in_ill1_ax. + rewrite <- map_map; apply S_ill_restr_weak_cntr with (1 := in_map _ _ _ H1); simpl. rewrite map_map. apply in_ill1_bang_l. apply in_ill1_perm with (£ p & £ q ⊸ £ r :: ((map (fun c => !⦑c⦒) Si ++ map £ Ga) ++ nil)). * rewrite app_nil_r; auto. * apply in_ill1_limp_l. - apply in_ill1_with_r; auto. - apply in_ill1_ax. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill)