CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Coq.Logic.Description.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_remove_list.
Require Import CPP_BiInt_enum.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* Random lemmas. *)
Lemma nat_remove_le_length : forall l (n : nat), length (remove Nat.eq_dec n l) <= length l.
Proof.
induction l.
- intros. simpl. reflexivity.
- intros. simpl. destruct (Nat.eq_dec n a).
* subst. apply le_S. apply IHl.
* simpl. apply le_n_S. apply IHl.
Qed.
Lemma nat_remove_In_smaller_length : forall (l : list nat) (n : nat),
List.In n l -> length (remove Nat.eq_dec n l) < length l.
Proof.
induction l.
- intros. inversion H.
- intros. simpl. destruct (Nat.eq_dec n a).
* subst. unfold lt. apply le_n_S. apply nat_remove_le_length.
* simpl. inversion H ; subst. exfalso ; apply n0 ; auto.
apply IHl in H0 ; lia.
Qed.
Lemma max_of_list : forall (l : list nat), ((l = []) -> False) -> (exists n, (List.In n l) /\
(forall m, List.In m l -> m <= n)).
Proof.
induction l.
- simpl. intros. exfalso. apply H. auto.
- intros. destruct l.
* exists a. split. apply in_eq. intros. inversion H0. subst. auto. inversion H1.
* assert (n :: l = [] -> False). intro. inversion H0. apply IHl in H0.
destruct H0. destruct H0. inversion H0.
+ subst. exists (Nat.max a x). split. pose (Nat.max_dec a x).
destruct s. rewrite e. apply in_eq. rewrite e. apply in_cons. apply in_eq.
intros. inversion H2. lia. pose (H1 m). apply l0 in H3. lia.
+ exists (Nat.max a x). split. pose (Nat.max_dec a x).
destruct s. rewrite e. apply in_eq. rewrite e. apply in_cons. apply in_cons. auto.
intros. inversion H3. lia. pose (H1 m). apply l0 in H4. lia.
Qed.
Lemma always_add_a_nat : forall (l : list nat), (NoDup l) -> (exists n, (NoDup (n :: l))).
Proof.
intros. destruct l.
- exists 0. apply NoDup_cons ; auto ; apply NoDup_nil.
- assert (J1: (n :: l = [] -> False) ). intro. inversion H0.
pose (max_of_list (n :: l) J1). destruct e. destruct H0. exists (S x).
apply NoDup_cons. intro. apply H1 in H2. lia. auto.
Qed.
Lemma no_list_all_nat : (exists (l : list nat), (NoDup l) /\ (forall (n : nat), List.In n l)) -> False.
Proof.
intros. destruct H. destruct H. pose (always_add_a_nat x H). destruct e.
assert (incl (x0 :: x) x). intro. intros. inversion H2. subst. pose (H0 a). auto.
auto. pose (@NoDup_incl_length nat (x0 :: x) x H1 H2). simpl in l. lia.
Qed.
Lemma list_all_pred_nat : forall n, exists l, (NoDup l) /\ (forall m, (m <= n) <-> List.In m l).
Proof.
induction n. exists [0]. split. apply NoDup_cons ; auto ; apply NoDup_nil.
intros. split ; intro. inversion H. subst. apply in_eq.
inversion H. subst. auto. inversion H0. destruct IHn. destruct H. exists ((S n) :: x).
intros. split. apply NoDup_cons. intro. apply H0 in H1. lia. auto.
split ; intros. inversion H1. subst. apply in_eq. subst. apply in_cons.
apply H0. auto. inversion H1. subst. auto. apply H0 in H2. lia.
Qed.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* Multiple disjunctions lemmas. *)
Fixpoint mult_disj (n : nat) (A : BPropF) : BPropF :=
match n with
| 0 => A
| S m => Or A (mult_disj m A)
end.
Lemma der_mult_disj_Bot : forall n Γ A,
BIH_rules (Γ, Or A (mult_disj n (Bot))) -> BIH_rules (Γ, A).
Proof.
induction n.
- simpl. intros. apply absorp_Or1. auto.
- simpl. intros.
apply MP with (ps:=[(Γ, Imp (Or A (Or (Bot) (mult_disj n (Bot)))) A);(Γ, Or A (Or (Bot) (mult_disj n (Bot))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, ((Or (Bot) (mult_disj n (Bot))) --> A) --> (Or A (Or (Bot) (mult_disj n (Bot))) --> A));(Γ, ((Or (Bot) (mult_disj n (Bot))) --> A))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ, (A --> A) --> ((Or (Bot) (mult_disj n (Bot))) --> A) --> (Or A (Or (Bot) (mult_disj n (Bot))) --> A));(Γ, A --> A)]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I.
apply RA4_I. exists A. exists (Or (Bot) (mult_disj n (Bot))). exists A. auto.
inversion H3. 2: inversion H4. subst. apply wimp_Id_gen. inversion H2. 2: inversion H3.
subst.
apply MP with (ps:=[(Γ, ((Bot) --> A) --> (Or (Bot) (mult_disj n (Bot)) --> A));
(Γ, (Bot) --> A)]). 2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Γ, (Or (Bot) (mult_disj n (Bot)) --> (Bot)) --> ((Bot) --> A) --> (Or (Bot) (mult_disj n (Bot)) --> A));
(Γ, Or (Bot) (mult_disj n (Bot)) --> (Bot))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Or (Bot) (mult_disj n (Bot))).
exists (Bot). exists A. auto. inversion H5. 2: inversion H6. subst.
clear H4. clear H5. clear H3. clear H1. clear H2. clear H0.
apply BIH_Deduction_Theorem with (s:=(Union _ Γ (Singleton _ (Or (Bot) (mult_disj n (Bot)))), Bot)) ; auto.
apply IHn. apply Id. apply IdRule_I. apply Union_intror. apply In_singleton.
inversion H4. 2: inversion H5. subst. apply wEFQ.
inversion H1. 2: inversion H2. subst. auto.
Qed.
Lemma mult_disj_Id : forall x y, (mult_disj x (Bot) = mult_disj y (Bot)) -> x = y.
Proof.
induction x.
- intros. simpl in H. destruct y. auto. simpl in H. destruct y. simpl in H. inversion H.
inversion H.
- induction y.
* intros. simpl in H. inversion H.
* intros. simpl in H. inversion H. apply IHx in H1. auto.
Qed.
Lemma mult_disj_dec0 : forall C,
(exists g, C = (mult_disj g (Bot))) \/ ((exists g, C = (mult_disj g (Bot))) -> False).
Proof.
induction C ; simpl ; auto. right ; intros ; destruct H. 3-4: right ; intros ; destruct H. 6-7: right ; intros ; destruct H.
induction x ; simpl in H ; inversion H.
left ; exists 0 ; auto.
induction x ; simpl in H ; inversion H.
induction x ; simpl in H ; inversion H.
destruct IHC1 ; destruct IHC2. destruct H. destruct H0 ; subst. destruct x ; simpl.
left. exists (S x0) ; simpl ; auto. right. intro. destruct H. destruct x1 ; simpl in H.
inversion H. inversion H. destruct H ; subst. destruct x ; simpl. destruct C2.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
left ; exists 1 ; simpl ; auto.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x ; simpl in H ; inversion H ; auto. apply H0. exists x ; auto.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x0 ; inversion H.
destruct H0 ;subst. destruct C1.
right ; intro. destruct H0. destruct x0 ; inversion H0.
left ; exists (S x) ; simpl ; auto.
1-5: right ; intro ; destruct H0 ; destruct x0 ; inversion H0.
right ; intro. destruct H1. destruct x ; simpl in H1 ; inversion H1 ; subst.
apply H ; exists 0 ; simpl ; auto.
induction x ; simpl in H ; inversion H.
induction x ; simpl in H ; inversion H.
Qed.
Lemma mult_disj_dec1 : forall C B,
(exists g, C = (Or B (mult_disj g (Bot)))) \/ ((exists g, C = (Or B (mult_disj g (Bot)))) -> False).
Proof.
destruct C ; simpl ; auto. 1-4: right ; intros ; destruct H ; inversion H. 2-3: right ; intros ; destruct H ; inversion H.
intros. destruct (eq_dec_form C1 B) ; subst. 2: right ; intro ; destruct H ; inversion H ; auto.
destruct (mult_disj_dec0 C2). destruct H ; subst. left ; exists x ; auto. right ; intro. destruct H0. inversion H0 ; subst.
apply H. exists x ; auto.
Qed.
Lemma mult_disj_dec : forall C A B,
(exists g, C = (Or A (Or B (mult_disj g (Bot))))) \/ ((exists g, C = (Or A (Or B (mult_disj g (Bot))))) -> False).
Proof.
destruct C ; simpl ; auto. 1-4: right ; intros ; destruct H ; inversion H. 2-3: right ; intros ; destruct H ; inversion H.
intros. destruct (eq_dec_form C1 A) ; subst. 2: right ; intro ; destruct H ; inversion H ; auto.
destruct (mult_disj_dec1 C2 B) ; subst. destruct H ; subst. left. exists x ; auto.
right; intro. destruct H0 ; subst. inversion H0 ; subst. apply H. exists x ; auto.
Qed.
Lemma too_many_disj00 : forall (n : nat) A B,
((exists (m k : nat), (m <= n) /\ (form_enum m = (Or A (Or B (mult_disj k (Bot)))))) -> False)
\/
(exists (m max : nat), (form_enum m = (Or A (Or B (mult_disj max (Bot)))) /\ (m <= n))
/\
(forall (o p : nat), ((form_enum p = (Or A (Or B (mult_disj o (Bot)))) /\ (p <= n)) ->
o <= max))).
Proof.
induction n.
- intros. remember (form_enum 0) as u.
+ destruct (mult_disj_dec u A B).
* destruct H. right. exists 0. exists x. repeat split ; auto.
subst. auto. intros. destruct H0. inversion H1. subst. clear H1.
rewrite H in H0. inversion H0. apply mult_disj_Id in H2. lia.
* left. intro. destruct H0. destruct H0. destruct H0. inversion H0. subst.
apply H. exists x0. auto.
- intros. remember (form_enum (S n)) as u.
+ destruct (mult_disj_dec u A B).
* destruct H. subst. right. pose (IHn A B). destruct o.
{ clear IHn. exists (S n). exists x. repeat split ; auto.
intros. destruct H1. inversion H2. subst. rewrite H in H1.
inversion H1. apply mult_disj_Id in H4. lia. subst. exfalso.
apply H0. exists p. exists o. split ; auto. }
{ clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
pose (Nat.max_dec x1 x). destruct s.
- exists x0. exists x1. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3.
apply mult_disj_Id in H6. lia. subst. apply H1 with (p:=p).
split ; auto.
- exists (S n). exists x. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3.
apply mult_disj_Id in H6. lia. subst. pose (H1 o p). destruct l.
split ; auto. lia. lia. }
* pose (IHn A B). destruct o.
{ left. intro. clear IHn. destruct H1. destruct H1. destruct H1. subst.
inversion H1. subst. apply H.
exists x0. auto. subst. apply H0. exists x. exists x0. split ; auto. }
{ right. clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
exists x. exists x0. repeat split ; auto. intros. destruct H3. inversion H4.
subst. exfalso. apply H. exists o ; auto. subst. apply H1 with (p:=p). split ; auto. }
Qed.
Lemma too_many_disj0 : forall (n : nat) A B,
(exists (m k : nat), (form_enum m = (Or A (Or B (mult_disj k (Bot)))) /\ (n <= m))).
Proof.
intros.
pose (too_many_disj00 n A B). destruct o.
- exists (form_index (Or A (Or B (mult_disj 0 (Bot))))). exists 0.
split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Or B (Bot))))) ; auto.
exfalso. assert (form_index (Or A (Or B (Bot))) < n). lia.
apply H. exists (form_index (Or A (Or B (Bot)))). exists 0. simpl.
split ; try lia. apply form_enum_index.
- destruct H. destruct H. destruct H. destruct H.
exists (form_index (Or A (Or B (mult_disj (S x0) (Bot))))).
exists (S x0). split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot))))))) ; auto.
assert ((form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot)))))) <= n). lia.
clear H2. pose (H0 (S x0) (form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot))))))).
assert (form_enum (form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot)))))) = (Or A (Or B (mult_disj (S x0) (Bot)))) /\
form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot))))) <= n). split.
apply form_enum_index. lia. apply l in H2. exfalso. lia.
Qed.
Lemma too_many_disj10 :forall (n : nat) A,
((exists (m k : nat), (m <= n) /\ (form_enum m = (Or A (mult_disj k (Bot))))) -> False)
\/
(exists (m max : nat), (form_enum m = (Or A (mult_disj max (Bot))) /\ (m <= n))
/\
(forall (o p : nat), ((form_enum p = (Or A (mult_disj o (Bot))) /\ (p <= n)) ->
o <= max))).
Proof.
induction n.
- intros. remember (form_enum 0) as u. destruct (mult_disj_dec1 u A).
* destruct H. right. exists 0. exists x. repeat split ; auto.
subst. auto. intros. destruct H0. inversion H1. subst. clear H1.
rewrite H in H0. inversion H0. apply mult_disj_Id in H2. lia.
* left. intro. destruct H0. destruct H0. destruct H0. inversion H0. subst.
apply H. exists x0. auto.
- intros. remember (form_enum (S n)) as u. destruct (mult_disj_dec1 u A).
* destruct H. subst. right. pose (IHn A). destruct o.
{ clear IHn. exists (S n). exists x. repeat split ; auto.
intros. destruct H1. inversion H2. subst. rewrite H in H1.
inversion H1. apply mult_disj_Id in H4. lia. subst. exfalso.
apply H0. exists p. exists o. split ; auto. }
{ clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
pose (Nat.max_dec x1 x). destruct s.
- exists x0. exists x1. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3. subst.
apply mult_disj_Id in H6. lia. subst. apply H1 with (p:=p).
split ; auto.
- exists (S n). exists x. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3.
apply mult_disj_Id in H6. lia. subst. pose (H1 o p). destruct l.
split ; auto. lia. lia. }
* pose (IHn A). destruct o.
{ left. intro. clear IHn. destruct H1. destruct H1. destruct H1. subst.
inversion H1. subst. apply H. exists x0. auto. subst. apply H0.
exists x. exists x0. split ; auto. }
{ right. clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
exists x. exists x0. repeat split ; auto. intros. destruct H3. inversion H4.
subst. exfalso. apply H. exists o ; auto.
subst. apply H1 with (p:=p). split ; auto. }
Qed.
Lemma too_many_disj1 : forall (n : nat) A,
(exists (m k : nat), (form_enum m = (Or A (mult_disj k (Bot))) /\ (n <= m))).
Proof.
intros.
pose (too_many_disj10 n A). destruct o.
- exists (form_index (Or A (mult_disj 0 (Bot)))). exists 0.
split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Bot)))) ; auto.
exfalso. assert ((form_index (Or A (Bot))) < n). lia.
apply H. exists (form_index (Or A (Bot))). exists 0. simpl.
split ; try lia. apply form_enum_index.
- destruct H. destruct H. destruct H. destruct H.
exists (form_index (Or A (mult_disj (S x0) (Bot)))).
exists (S x0). split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Or (Bot) (mult_disj x0 (Bot)))))) ; auto.
assert ((form_index (Or A (Or (Bot) (mult_disj x0 (Bot))))) <= n). lia.
clear H2. pose (H0 (S x0) (form_index (Or A (Or (Bot) (mult_disj x0 (Bot)))))).
assert (form_enum (form_index (Or A (Or (Bot) (mult_disj x0 (Bot))))) = (Or A (mult_disj (S x0) (Bot))) /\
form_index (Or A (Or (Bot) (mult_disj x0 (Bot)))) <= n). split.
simpl. apply form_enum_index. lia. apply l in H2. exfalso. lia.
Qed.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* List of disjunctions. *)
Lemma Id_list_disj : forall Γ l0 l1,
BIH_rules (Γ, list_disj l0 --> list_disj (l0 ++ l1)).
Proof.
induction l0 ; intros.
- simpl. apply wEFQ.
- simpl. apply wmonotL_Or. apply IHl0.
Qed.
Lemma list_disj_app : forall l0 Γ A l1,
BIH_rules (Γ, A --> list_disj (l0 ++ l1)) -> BIH_rules (Γ, A --> (Or (list_disj l0) (list_disj l1))).
Proof.
induction l0.
- simpl. intros.
apply MP with (ps:=[(Γ, ((list_disj l1) --> Or (Bot) (list_disj l1)) --> (A --> Or (Bot) (list_disj l1)));(Γ, (list_disj l1) --> Or (Bot) (list_disj l1))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> (list_disj l1)) --> ((list_disj l1) --> Or (Bot) (list_disj l1)) --> (A --> Or (Bot) (list_disj l1)));(Γ,A --> (list_disj l1))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists A. exists (list_disj l1). exists (Or (Bot) (list_disj l1)). auto. inversion H2.
2: inversion H3. subst. assumption. inversion H1. 2: inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists (Bot). exists (list_disj l1). auto.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (A --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or a (list_disj (l0 ++ l1))) --> (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (A --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, A --> Or a (list_disj (l0 ++ l1)))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists A. exists (Or a (list_disj (l0 ++ l1))). exists (Or (Or a (list_disj l0)) (list_disj l1)).
auto. inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst.
apply MP with (ps:=[(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or (Or a (list_disj l0)) (list_disj l1)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ, (Or a (list_disj (l0 ++ l1)) --> Or a (Or (list_disj l0) (list_disj l1))) --> (Or a (Or (list_disj l0) (list_disj l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, (Or a (list_disj (l0 ++ l1)) --> Or a (Or (list_disj l0) (list_disj l1))))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Or a (list_disj (l0 ++ l1))). exists (Or a (Or (list_disj l0) (list_disj l1))).
exists (Or (Or a (list_disj l0)) (list_disj l1)). auto. inversion H4. 2: inversion H5.
subst. apply wmonotL_Or. apply IHl0. apply wimp_Id_gen. inversion H3. 2: inversion H4. subst.
remember (list_disj l0) as E. remember (list_disj l1) as F.
apply MP with (ps:=[(Γ, ((Or E F) --> Or (Or a E) F) --> (Or a (Or E F) --> Or (Or a E) F));
(Γ, ((Or E F) --> Or (Or a E) F))]). 2: apply MPRule_I. intros. inversion H4. rewrite <- H5.
apply MP with (ps:=[(Γ, (a --> Or (Or a E) F) --> ((Or E F) --> Or (Or a E) F) --> (Or a (Or E F) --> Or (Or a E) F));
(Γ, (a --> Or (Or a E) F))]). 2: apply MPRule_I. intros. inversion H6. rewrite <- H7.
apply Ax. apply AxRule_I. apply RA4_I. exists a. exists (Or E F). exists (Or (Or a E) F).
auto. inversion H7. 2: inversion H8. rewrite <- H8.
apply MP with (ps:=[(Γ, ((Or a E) --> Or (Or a E) F) --> (a --> Or (Or a E) F));(Γ, ((Or a E) --> Or (Or a E) F))]).
2: apply MPRule_I. intros. inversion H9. rewrite <- H10.
apply MP with (ps:=[(Γ, (a --> (Or a E)) --> ((Or a E) --> Or (Or a E) F) --> (a --> Or (Or a E) F));(Γ, a --> (Or a E))]).
2: apply MPRule_I. intros. inversion H11. rewrite <- H12. apply Ax. apply AxRule_I.
apply RA1_I. exists a. exists (Or a E). exists (Or (Or a E) F). auto.
inversion H12. 2: inversion H13. rewrite <- H13. apply Ax. apply AxRule_I. apply RA2_I.
exists a. exists E. auto. inversion H10. 2: inversion H11. rewrite <- H11. apply Ax.
apply AxRule_I. apply RA2_I. exists (Or a E). exists F. auto. inversion H5. 2: inversion H6.
rewrite <- H6. apply wmonotR_Or. apply Ax. apply AxRule_I. apply RA3_I. exists a. exists E. auto.
Qed.
Lemma list_disj_app0 : forall l0 Γ A l1,
BIH_rules (Γ, A --> (Or (list_disj l0) (list_disj l1))) -> BIH_rules (Γ, A --> list_disj (l0 ++ l1)).
Proof.
induction l0.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or (Bot) (list_disj l1) --> list_disj l1) --> (A --> list_disj l1));
(Γ, Or (Bot) (list_disj l1) --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or (Bot) (list_disj l1)) --> (Or (Bot) (list_disj l1) --> list_disj l1) --> (A --> list_disj l1));
(Γ, A --> Or (Bot) (list_disj l1))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or (Bot) (list_disj l1)).
exists (list_disj l1). auto. inversion H2. 2: inversion H3. subst. auto. inversion H1.
2: inversion H2. subst.
apply MP with (ps:=[(Γ, ((list_disj l1) --> list_disj l1) --> (Or (Bot) (list_disj l1) --> list_disj l1));
(Γ, (list_disj l1) --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ, (Bot --> list_disj l1) --> ((list_disj l1) --> list_disj l1) --> (Or (Bot) (list_disj l1) --> list_disj l1));
(Γ, Bot --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists (Bot). exists (list_disj l1).
exists (list_disj l1). auto. inversion H4. 2: inversion H5. subst. apply wEFQ.
inversion H3. 2: inversion H4. subst. apply wimp_Id_gen.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))) --> (A --> Or a (list_disj (l0 ++ l1))));
(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or (Or a (list_disj l0)) (list_disj l1)) --> (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))) --> (A --> Or a (list_disj (l0 ++ l1))));
(Γ, A --> Or (Or a (list_disj l0)) (list_disj l1))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists A. exists (Or (Or a (list_disj l0)) (list_disj l1)). exists (Or a (list_disj (l0 ++ l1))).
auto. inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst.
apply MP with (ps:=[(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or a (list_disj (l0 ++ l1))) --> (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))));
(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or a (list_disj (l0 ++ l1))))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (Or (list_disj l0) (list_disj l1))) --> (Or a (Or (list_disj l0) (list_disj l1)) --> Or a (list_disj (l0 ++ l1))) --> (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))));
(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (Or (list_disj l0) (list_disj l1))))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Or (Or a (list_disj l0)) (list_disj l1)).
exists (Or a (Or (list_disj l0) (list_disj l1))). exists (Or a (list_disj (l0 ++ l1))).
auto. inversion H4. 2: inversion H5.
subst. remember (list_disj l0) as E. remember (list_disj l1) as F.
apply MP with (ps:=[(Γ, (F --> Or a (Or E F)) --> (Or (Or a E) F --> Or a (Or E F)));
(Γ, F --> Or a (Or E F))]). 2: apply MPRule_I. intros. inversion H5. rewrite <- H6.
apply MP with (ps:=[(Γ, ((Or a E) --> Or a (Or E F)) --> (F --> Or a (Or E F)) --> (Or (Or a E) F --> Or a (Or E F)));
(Γ, ((Or a E) --> Or a (Or E F)))]). 2: apply MPRule_I. intros. inversion H7. rewrite <- H8.
apply Ax. apply AxRule_I. apply RA4_I. exists (Or a E). exists F. exists (Or a (Or E F)).
auto. inversion H8. 2: inversion H9. rewrite <- H9. apply wmonotL_Or. apply Ax.
apply AxRule_I. apply RA2_I. exists E. exists F. auto. inversion H6. 2: inversion H7.
rewrite <- H7.
apply MP with (ps:=[(Γ, ((Or E F) --> Or a (Or E F)) --> (F --> Or a (Or E F)));(Γ, ((Or E F) --> Or a (Or E F)))]).
2: apply MPRule_I. intros. inversion H8. rewrite <- H9.
apply MP with (ps:=[(Γ, (F --> (Or E F)) --> ((Or E F) --> Or a (Or E F)) --> (F --> Or a (Or E F)));(Γ, F --> (Or E F))]).
2: apply MPRule_I. intros. inversion H10. rewrite <- H11. apply Ax. apply AxRule_I.
apply RA1_I. exists F. exists (Or E F). exists (Or a (Or E F)). auto.
inversion H11. 2: inversion H12. rewrite <- H12. apply Ax. apply AxRule_I. apply RA3_I.
exists E. exists F. auto. inversion H9. 2: inversion H10. rewrite <- H10. apply Ax.
apply AxRule_I. apply RA3_I. exists a. exists (Or E F). auto. inversion H3. 2: inversion H4.
rewrite <- H4. apply wmonotL_Or. apply IHl0. apply wimp_Id_gen.
Qed.
Lemma list_disj_remove_app : forall l0 l1 Γ A,
BIH_rules (Γ, list_disj (l0 ++ remove_list l0 l1) --> Or A (list_disj (l0 ++ remove eq_dec_form A (remove_list l0 l1)))).
Proof.
induction l0.
- simpl. intros. apply remove_disj.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))) --> (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))));
(Γ,Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1))))))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ, (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))) --> (Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))) --> (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))));
(Γ,(Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I.
exists (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))).
exists (Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))).
exists (Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))). auto.
inversion H1. 2: inversion H2. subst.
{ simpl. apply wmonotL_Or. clear H1. clear H0. clear H.
remember (remove eq_dec_form a (remove_list l0 l1)) as E.
apply MP with (ps:=[(Γ, (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E))) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))) --> (list_disj (l0 ++ E) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))));
(Γ, (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E))) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))))]).
2: apply MPRule_I. intros. inversion H. rewrite <- H0.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))) --> (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E))) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))) --> (list_disj (l0 ++ E) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))));
(Γ, (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))))]).
2: apply MPRule_I. intros. inversion H1. rewrite <- H2. apply Ax. apply AxRule_I.
apply RA1_I. exists (list_disj (l0 ++ E)). exists (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))).
exists (Or A (list_disj (l0 ++ remove eq_dec_form A E))). auto. inversion H2. rewrite <- H3.
{ simpl. apply MP with (ps:=[(Γ, ((Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))) --> (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))));
(Γ, ((Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))))]).
2: apply MPRule_I. intros. inversion H4. rewrite <- H5.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ E) --> (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E))))) --> ((Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))) --> (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))));
(Γ, (list_disj (l0 ++ E) --> (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E))))))]).
2: apply MPRule_I. intros. inversion H6. rewrite <- H7. apply Ax. apply AxRule_I. apply RA1_I.
exists (list_disj (l0 ++ E)). exists (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))).
exists (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))). auto.
inversion H7. 2: inversion H8. rewrite <- H8.
{ remember (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) as F.
apply MP with (ps:=[(Γ, ((Or (list_disj l0) (list_disj E)) --> F) --> (list_disj (l0 ++ E) --> F));
(Γ, ((Or (list_disj l0) (list_disj E)) --> F))]). 2: apply MPRule_I. intros.
inversion H9. rewrite <- H10.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ E) --> (Or (list_disj l0) (list_disj E))) --> ((Or (list_disj l0) (list_disj E)) --> F) --> (list_disj (l0 ++ E) --> F));
(Γ, list_disj (l0 ++ E) --> (Or (list_disj l0) (list_disj E)))]). 2: apply MPRule_I. intros.
inversion H11. rewrite <- H12. apply Ax. apply AxRule_I. apply RA1_I.
exists (list_disj (l0 ++ E)). exists (Or (list_disj l0) (list_disj E)). exists F. auto.
inversion H12. 2: inversion H13. rewrite <- H13. apply list_disj_app. apply wimp_Id_gen.
inversion H10. 2: inversion H11. rewrite <- H11. clear H11. clear H10.
clear H9. clear H8. clear H7. clear H6. clear H5. clear H0. clear H4.
clear H3. clear H2. clear H1. clear H. rewrite HeqF. apply wmonotL_Or.
apply remove_disj. }
inversion H5. 2: inversion H6. rewrite <- H6. remember (list_disj l0) as D.
remember (list_disj (remove eq_dec_form A E)) as F.
apply MP with (ps:=[(Γ, (Or A F --> Or A (Or D F)) --> (Or D (Or A F) --> Or A (Or D F)));(Γ, (Or A F) --> Or A (Or D F))]).
2: apply MPRule_I. intros. inversion H7. rewrite <- H8.
apply MP with (ps:=[(Γ, (D --> Or A (Or D F)) --> (Or A F --> Or A (Or D F)) --> (Or D (Or A F) --> Or A (Or D F)));(Γ, D --> Or A (Or D F))]).
2: apply MPRule_I. intros. inversion H9. rewrite <- H10. apply Ax. apply AxRule_I.
apply RA4_I. exists D. exists (Or A F). exists (Or A (Or D F)). auto. inversion H10. 2: inversion H11.
rewrite <- H11.
apply MP with (ps:=[(Γ, ((Or D F) --> Or A (Or D F)) --> (D --> Or A (Or D F)));(Γ, ((Or D F) --> Or A (Or D F)))]).
2: apply MPRule_I. intros. inversion H12. rewrite <- H13.
apply MP with (ps:=[(Γ, (D --> (Or D F)) --> ((Or D F) --> Or A (Or D F)) --> (D --> Or A (Or D F)));(Γ, D --> (Or D F))]).
2: apply MPRule_I. intros. inversion H14. rewrite <- H15. apply Ax. apply AxRule_I.
apply RA1_I. exists D. exists (Or D F). exists (Or A (Or D F)). auto. inversion H15.
rewrite <- H16. apply Ax. apply AxRule_I. apply RA2_I. exists D. exists F. auto.
inversion H16. inversion H13. rewrite <- H14. apply Ax. apply AxRule_I. apply RA3_I.
exists A. exists (Or D F). auto. inversion H14. inversion H8. rewrite <- H9.
apply wmonotL_Or. apply Ax. apply AxRule_I. apply RA3_I. exists D. exists F. auto.
inversion H9. }
inversion H3. inversion H0. 2: inversion H1. rewrite <- H1. apply wmonotL_Or. apply list_disj_app0.
apply wimp_Id_gen. }
inversion H0. 2: inversion H1. subst.
remember ((list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1))))) as E.
apply MP with (ps:=[(Γ, ((Or A E) --> Or A (Or a E)) --> (Or a (Or A E) --> Or A (Or a E)));
(Γ, ((Or A E) --> Or A (Or a E)))]). 2: apply MPRule_I. intros. inversion H1. rewrite <- H2.
apply MP with (ps:=[(Γ, (a --> Or A (Or a E)) --> ((Or A E) --> Or A (Or a E)) --> (Or a (Or A E) --> Or A (Or a E)));
(Γ, (a --> Or A (Or a E)))]). 2: apply MPRule_I. intros. inversion H3. rewrite <- H4. clear H4.
clear H2. apply Ax. apply AxRule_I. apply RA4_I. exists a. exists (Or A E).
exists (Or A (Or a E)). auto. inversion H4. 2: inversion H5. rewrite <- H5.
apply MP with (ps:=[(Γ, ((Or a E) --> Or A (Or a E)) --> (a --> Or A (Or a E))); (Γ, ((Or a E) --> Or A (Or a E)))]).
2: apply MPRule_I. intros. inversion H6. rewrite <- H7.
apply MP with (ps:=[(Γ, (a --> (Or a E)) --> ((Or a E) --> Or A (Or a E)) --> (a --> Or A (Or a E))); (Γ, a --> (Or a E))]).
2: apply MPRule_I. intros. inversion H8. rewrite <- H9. apply Ax. apply AxRule_I. apply RA1_I.
exists a. exists (Or a E). exists (Or A (Or a E)). auto. inversion H9.
rewrite <- H10. 2: inversion H10. apply Ax. apply AxRule_I. apply RA2_I.
exists a. exists E. auto. inversion H7. 2: inversion H8. rewrite <- H8.
apply Ax. apply AxRule_I. apply RA3_I. exists A. exists (Or a E). auto.
inversion H2. rewrite <- H3. apply wmonotL_Or. apply Ax. apply AxRule_I.
apply RA3_I. exists a. exists E. auto. inversion H3.
Qed.
Lemma Id_list_disj_remove : forall Γ l0 l1,
BIH_rules (Γ, list_disj l1 --> list_disj (l0 ++ remove_list l0 l1)).
Proof.
induction l0.
- intros. simpl. apply wimp_Id_gen.
- simpl. intros.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ remove_list l0 l1) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (list_disj l1 --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ, list_disj (l0 ++ remove_list l0 l1) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1))))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ, (list_disj l1 --> list_disj (l0 ++ remove_list l0 l1)) --> (list_disj (l0 ++ remove_list l0 l1) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (list_disj l1 --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ,list_disj l1 --> list_disj (l0 ++ remove_list l0 l1))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (list_disj l1). exists (list_disj (l0 ++ remove_list l0 l1)).
exists (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))). auto.
inversion H1. 2: inversion H2. subst. apply IHl0. inversion H0. subst.
clear H. clear H0. apply list_disj_remove_app. inversion H1.
Qed.
Lemma der_list_disj_remove1 : forall Γ A l0 l1,
(BIH_rules (Γ, A --> list_disj l0)) ->
(BIH_rules (Γ, A --> list_disj (l0 ++ remove_list l0 l1))).
Proof.
intros Γ A. induction l0.
- simpl. intros.
apply MP with (ps:=[(Γ, (Bot --> list_disj l1) --> (A --> list_disj l1));
(Γ, Bot --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Bot) --> (Bot --> list_disj l1) --> (A --> list_disj l1));
(Γ, A --> Bot)]). 2: apply MPRule_I. intros. inversion H1. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Bot). exists (list_disj l1).
auto. inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst. apply wEFQ.
- intros. subst. simpl. simpl in H.
apply MP with (ps:=[(Γ, (Or a (list_disj l0) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (A --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ, (Or a (list_disj l0) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or a (list_disj l0)) --> (Or a (list_disj l0) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (A --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ, A --> Or a (list_disj l0))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or a (list_disj l0)).
exists (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))). auto.
inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst. clear H0. clear H1. apply wmonotL_Or. apply Id_list_disj.
Qed.
Lemma der_list_disj_remove2 : forall Γ A l0 l1,
(BIH_rules (Γ, A --> list_disj l1)) ->
(BIH_rules (Γ, A --> list_disj (l0 ++ remove_list l0 l1))).
Proof.
intros.
apply MP with (ps:=[(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (A --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> list_disj l1) --> (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (A --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, A --> list_disj l1)]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists A. exists (list_disj l1). exists (list_disj (l0 ++ (remove_list l0 l1))).
auto. inversion H2. 2 : inversion H3. subst. auto. inversion H1. subst. 2: inversion H2.
clear H0. clear H1.
apply MP with (ps:=[(Γ, ((list_disj (l0 ++ (remove_list l0 l1))) --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, (list_disj (l0 ++ (remove_list l0 l1))) --> (list_disj (l0 ++ (remove_list l0 l1))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))) --> ((list_disj (l0 ++ (remove_list l0 l1))) --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists (list_disj l1). exists ((list_disj (l0 ++ (remove_list l0 l1)))).
exists (list_disj (l0 ++ (remove_list l0 l1))). auto. inversion H2.
2: inversion H3. subst. clear H1. clear H2. clear H0. apply Id_list_disj_remove.
inversion H1. 2: inversion H2. subst. clear H0. clear H1. apply wimp_Id_gen.
Qed.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Coq.Logic.Description.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_remove_list.
Require Import CPP_BiInt_enum.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* Random lemmas. *)
Lemma nat_remove_le_length : forall l (n : nat), length (remove Nat.eq_dec n l) <= length l.
Proof.
induction l.
- intros. simpl. reflexivity.
- intros. simpl. destruct (Nat.eq_dec n a).
* subst. apply le_S. apply IHl.
* simpl. apply le_n_S. apply IHl.
Qed.
Lemma nat_remove_In_smaller_length : forall (l : list nat) (n : nat),
List.In n l -> length (remove Nat.eq_dec n l) < length l.
Proof.
induction l.
- intros. inversion H.
- intros. simpl. destruct (Nat.eq_dec n a).
* subst. unfold lt. apply le_n_S. apply nat_remove_le_length.
* simpl. inversion H ; subst. exfalso ; apply n0 ; auto.
apply IHl in H0 ; lia.
Qed.
Lemma max_of_list : forall (l : list nat), ((l = []) -> False) -> (exists n, (List.In n l) /\
(forall m, List.In m l -> m <= n)).
Proof.
induction l.
- simpl. intros. exfalso. apply H. auto.
- intros. destruct l.
* exists a. split. apply in_eq. intros. inversion H0. subst. auto. inversion H1.
* assert (n :: l = [] -> False). intro. inversion H0. apply IHl in H0.
destruct H0. destruct H0. inversion H0.
+ subst. exists (Nat.max a x). split. pose (Nat.max_dec a x).
destruct s. rewrite e. apply in_eq. rewrite e. apply in_cons. apply in_eq.
intros. inversion H2. lia. pose (H1 m). apply l0 in H3. lia.
+ exists (Nat.max a x). split. pose (Nat.max_dec a x).
destruct s. rewrite e. apply in_eq. rewrite e. apply in_cons. apply in_cons. auto.
intros. inversion H3. lia. pose (H1 m). apply l0 in H4. lia.
Qed.
Lemma always_add_a_nat : forall (l : list nat), (NoDup l) -> (exists n, (NoDup (n :: l))).
Proof.
intros. destruct l.
- exists 0. apply NoDup_cons ; auto ; apply NoDup_nil.
- assert (J1: (n :: l = [] -> False) ). intro. inversion H0.
pose (max_of_list (n :: l) J1). destruct e. destruct H0. exists (S x).
apply NoDup_cons. intro. apply H1 in H2. lia. auto.
Qed.
Lemma no_list_all_nat : (exists (l : list nat), (NoDup l) /\ (forall (n : nat), List.In n l)) -> False.
Proof.
intros. destruct H. destruct H. pose (always_add_a_nat x H). destruct e.
assert (incl (x0 :: x) x). intro. intros. inversion H2. subst. pose (H0 a). auto.
auto. pose (@NoDup_incl_length nat (x0 :: x) x H1 H2). simpl in l. lia.
Qed.
Lemma list_all_pred_nat : forall n, exists l, (NoDup l) /\ (forall m, (m <= n) <-> List.In m l).
Proof.
induction n. exists [0]. split. apply NoDup_cons ; auto ; apply NoDup_nil.
intros. split ; intro. inversion H. subst. apply in_eq.
inversion H. subst. auto. inversion H0. destruct IHn. destruct H. exists ((S n) :: x).
intros. split. apply NoDup_cons. intro. apply H0 in H1. lia. auto.
split ; intros. inversion H1. subst. apply in_eq. subst. apply in_cons.
apply H0. auto. inversion H1. subst. auto. apply H0 in H2. lia.
Qed.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* Multiple disjunctions lemmas. *)
Fixpoint mult_disj (n : nat) (A : BPropF) : BPropF :=
match n with
| 0 => A
| S m => Or A (mult_disj m A)
end.
Lemma der_mult_disj_Bot : forall n Γ A,
BIH_rules (Γ, Or A (mult_disj n (Bot))) -> BIH_rules (Γ, A).
Proof.
induction n.
- simpl. intros. apply absorp_Or1. auto.
- simpl. intros.
apply MP with (ps:=[(Γ, Imp (Or A (Or (Bot) (mult_disj n (Bot)))) A);(Γ, Or A (Or (Bot) (mult_disj n (Bot))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, ((Or (Bot) (mult_disj n (Bot))) --> A) --> (Or A (Or (Bot) (mult_disj n (Bot))) --> A));(Γ, ((Or (Bot) (mult_disj n (Bot))) --> A))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ, (A --> A) --> ((Or (Bot) (mult_disj n (Bot))) --> A) --> (Or A (Or (Bot) (mult_disj n (Bot))) --> A));(Γ, A --> A)]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I.
apply RA4_I. exists A. exists (Or (Bot) (mult_disj n (Bot))). exists A. auto.
inversion H3. 2: inversion H4. subst. apply wimp_Id_gen. inversion H2. 2: inversion H3.
subst.
apply MP with (ps:=[(Γ, ((Bot) --> A) --> (Or (Bot) (mult_disj n (Bot)) --> A));
(Γ, (Bot) --> A)]). 2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Γ, (Or (Bot) (mult_disj n (Bot)) --> (Bot)) --> ((Bot) --> A) --> (Or (Bot) (mult_disj n (Bot)) --> A));
(Γ, Or (Bot) (mult_disj n (Bot)) --> (Bot))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Or (Bot) (mult_disj n (Bot))).
exists (Bot). exists A. auto. inversion H5. 2: inversion H6. subst.
clear H4. clear H5. clear H3. clear H1. clear H2. clear H0.
apply BIH_Deduction_Theorem with (s:=(Union _ Γ (Singleton _ (Or (Bot) (mult_disj n (Bot)))), Bot)) ; auto.
apply IHn. apply Id. apply IdRule_I. apply Union_intror. apply In_singleton.
inversion H4. 2: inversion H5. subst. apply wEFQ.
inversion H1. 2: inversion H2. subst. auto.
Qed.
Lemma mult_disj_Id : forall x y, (mult_disj x (Bot) = mult_disj y (Bot)) -> x = y.
Proof.
induction x.
- intros. simpl in H. destruct y. auto. simpl in H. destruct y. simpl in H. inversion H.
inversion H.
- induction y.
* intros. simpl in H. inversion H.
* intros. simpl in H. inversion H. apply IHx in H1. auto.
Qed.
Lemma mult_disj_dec0 : forall C,
(exists g, C = (mult_disj g (Bot))) \/ ((exists g, C = (mult_disj g (Bot))) -> False).
Proof.
induction C ; simpl ; auto. right ; intros ; destruct H. 3-4: right ; intros ; destruct H. 6-7: right ; intros ; destruct H.
induction x ; simpl in H ; inversion H.
left ; exists 0 ; auto.
induction x ; simpl in H ; inversion H.
induction x ; simpl in H ; inversion H.
destruct IHC1 ; destruct IHC2. destruct H. destruct H0 ; subst. destruct x ; simpl.
left. exists (S x0) ; simpl ; auto. right. intro. destruct H. destruct x1 ; simpl in H.
inversion H. inversion H. destruct H ; subst. destruct x ; simpl. destruct C2.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
left ; exists 1 ; simpl ; auto.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x ; simpl in H ; inversion H ; auto. apply H0. exists x ; auto.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x ; inversion H. destruct x ; inversion H2.
right ; intro. destruct H. destruct x0 ; inversion H.
destruct H0 ;subst. destruct C1.
right ; intro. destruct H0. destruct x0 ; inversion H0.
left ; exists (S x) ; simpl ; auto.
1-5: right ; intro ; destruct H0 ; destruct x0 ; inversion H0.
right ; intro. destruct H1. destruct x ; simpl in H1 ; inversion H1 ; subst.
apply H ; exists 0 ; simpl ; auto.
induction x ; simpl in H ; inversion H.
induction x ; simpl in H ; inversion H.
Qed.
Lemma mult_disj_dec1 : forall C B,
(exists g, C = (Or B (mult_disj g (Bot)))) \/ ((exists g, C = (Or B (mult_disj g (Bot)))) -> False).
Proof.
destruct C ; simpl ; auto. 1-4: right ; intros ; destruct H ; inversion H. 2-3: right ; intros ; destruct H ; inversion H.
intros. destruct (eq_dec_form C1 B) ; subst. 2: right ; intro ; destruct H ; inversion H ; auto.
destruct (mult_disj_dec0 C2). destruct H ; subst. left ; exists x ; auto. right ; intro. destruct H0. inversion H0 ; subst.
apply H. exists x ; auto.
Qed.
Lemma mult_disj_dec : forall C A B,
(exists g, C = (Or A (Or B (mult_disj g (Bot))))) \/ ((exists g, C = (Or A (Or B (mult_disj g (Bot))))) -> False).
Proof.
destruct C ; simpl ; auto. 1-4: right ; intros ; destruct H ; inversion H. 2-3: right ; intros ; destruct H ; inversion H.
intros. destruct (eq_dec_form C1 A) ; subst. 2: right ; intro ; destruct H ; inversion H ; auto.
destruct (mult_disj_dec1 C2 B) ; subst. destruct H ; subst. left. exists x ; auto.
right; intro. destruct H0 ; subst. inversion H0 ; subst. apply H. exists x ; auto.
Qed.
Lemma too_many_disj00 : forall (n : nat) A B,
((exists (m k : nat), (m <= n) /\ (form_enum m = (Or A (Or B (mult_disj k (Bot)))))) -> False)
\/
(exists (m max : nat), (form_enum m = (Or A (Or B (mult_disj max (Bot)))) /\ (m <= n))
/\
(forall (o p : nat), ((form_enum p = (Or A (Or B (mult_disj o (Bot)))) /\ (p <= n)) ->
o <= max))).
Proof.
induction n.
- intros. remember (form_enum 0) as u.
+ destruct (mult_disj_dec u A B).
* destruct H. right. exists 0. exists x. repeat split ; auto.
subst. auto. intros. destruct H0. inversion H1. subst. clear H1.
rewrite H in H0. inversion H0. apply mult_disj_Id in H2. lia.
* left. intro. destruct H0. destruct H0. destruct H0. inversion H0. subst.
apply H. exists x0. auto.
- intros. remember (form_enum (S n)) as u.
+ destruct (mult_disj_dec u A B).
* destruct H. subst. right. pose (IHn A B). destruct o.
{ clear IHn. exists (S n). exists x. repeat split ; auto.
intros. destruct H1. inversion H2. subst. rewrite H in H1.
inversion H1. apply mult_disj_Id in H4. lia. subst. exfalso.
apply H0. exists p. exists o. split ; auto. }
{ clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
pose (Nat.max_dec x1 x). destruct s.
- exists x0. exists x1. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3.
apply mult_disj_Id in H6. lia. subst. apply H1 with (p:=p).
split ; auto.
- exists (S n). exists x. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3.
apply mult_disj_Id in H6. lia. subst. pose (H1 o p). destruct l.
split ; auto. lia. lia. }
* pose (IHn A B). destruct o.
{ left. intro. clear IHn. destruct H1. destruct H1. destruct H1. subst.
inversion H1. subst. apply H.
exists x0. auto. subst. apply H0. exists x. exists x0. split ; auto. }
{ right. clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
exists x. exists x0. repeat split ; auto. intros. destruct H3. inversion H4.
subst. exfalso. apply H. exists o ; auto. subst. apply H1 with (p:=p). split ; auto. }
Qed.
Lemma too_many_disj0 : forall (n : nat) A B,
(exists (m k : nat), (form_enum m = (Or A (Or B (mult_disj k (Bot)))) /\ (n <= m))).
Proof.
intros.
pose (too_many_disj00 n A B). destruct o.
- exists (form_index (Or A (Or B (mult_disj 0 (Bot))))). exists 0.
split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Or B (Bot))))) ; auto.
exfalso. assert (form_index (Or A (Or B (Bot))) < n). lia.
apply H. exists (form_index (Or A (Or B (Bot)))). exists 0. simpl.
split ; try lia. apply form_enum_index.
- destruct H. destruct H. destruct H. destruct H.
exists (form_index (Or A (Or B (mult_disj (S x0) (Bot))))).
exists (S x0). split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot))))))) ; auto.
assert ((form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot)))))) <= n). lia.
clear H2. pose (H0 (S x0) (form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot))))))).
assert (form_enum (form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot)))))) = (Or A (Or B (mult_disj (S x0) (Bot)))) /\
form_index (Or A (Or B (Or (Bot) (mult_disj x0 (Bot))))) <= n). split.
apply form_enum_index. lia. apply l in H2. exfalso. lia.
Qed.
Lemma too_many_disj10 :forall (n : nat) A,
((exists (m k : nat), (m <= n) /\ (form_enum m = (Or A (mult_disj k (Bot))))) -> False)
\/
(exists (m max : nat), (form_enum m = (Or A (mult_disj max (Bot))) /\ (m <= n))
/\
(forall (o p : nat), ((form_enum p = (Or A (mult_disj o (Bot))) /\ (p <= n)) ->
o <= max))).
Proof.
induction n.
- intros. remember (form_enum 0) as u. destruct (mult_disj_dec1 u A).
* destruct H. right. exists 0. exists x. repeat split ; auto.
subst. auto. intros. destruct H0. inversion H1. subst. clear H1.
rewrite H in H0. inversion H0. apply mult_disj_Id in H2. lia.
* left. intro. destruct H0. destruct H0. destruct H0. inversion H0. subst.
apply H. exists x0. auto.
- intros. remember (form_enum (S n)) as u. destruct (mult_disj_dec1 u A).
* destruct H. subst. right. pose (IHn A). destruct o.
{ clear IHn. exists (S n). exists x. repeat split ; auto.
intros. destruct H1. inversion H2. subst. rewrite H in H1.
inversion H1. apply mult_disj_Id in H4. lia. subst. exfalso.
apply H0. exists p. exists o. split ; auto. }
{ clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
pose (Nat.max_dec x1 x). destruct s.
- exists x0. exists x1. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3. subst.
apply mult_disj_Id in H6. lia. subst. apply H1 with (p:=p).
split ; auto.
- exists (S n). exists x. repeat split ; auto. intros. destruct H3.
inversion H4. subst. rewrite H in H3. inversion H3.
apply mult_disj_Id in H6. lia. subst. pose (H1 o p). destruct l.
split ; auto. lia. lia. }
* pose (IHn A). destruct o.
{ left. intro. clear IHn. destruct H1. destruct H1. destruct H1. subst.
inversion H1. subst. apply H. exists x0. auto. subst. apply H0.
exists x. exists x0. split ; auto. }
{ right. clear IHn. destruct H0. destruct H0. destruct H0. destruct H0.
exists x. exists x0. repeat split ; auto. intros. destruct H3. inversion H4.
subst. exfalso. apply H. exists o ; auto.
subst. apply H1 with (p:=p). split ; auto. }
Qed.
Lemma too_many_disj1 : forall (n : nat) A,
(exists (m k : nat), (form_enum m = (Or A (mult_disj k (Bot))) /\ (n <= m))).
Proof.
intros.
pose (too_many_disj10 n A). destruct o.
- exists (form_index (Or A (mult_disj 0 (Bot)))). exists 0.
split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Bot)))) ; auto.
exfalso. assert ((form_index (Or A (Bot))) < n). lia.
apply H. exists (form_index (Or A (Bot))). exists 0. simpl.
split ; try lia. apply form_enum_index.
- destruct H. destruct H. destruct H. destruct H.
exists (form_index (Or A (mult_disj (S x0) (Bot)))).
exists (S x0). split. apply form_enum_index.
destruct (Nat.le_decidable n (form_index (Or A (Or (Bot) (mult_disj x0 (Bot)))))) ; auto.
assert ((form_index (Or A (Or (Bot) (mult_disj x0 (Bot))))) <= n). lia.
clear H2. pose (H0 (S x0) (form_index (Or A (Or (Bot) (mult_disj x0 (Bot)))))).
assert (form_enum (form_index (Or A (Or (Bot) (mult_disj x0 (Bot))))) = (Or A (mult_disj (S x0) (Bot))) /\
form_index (Or A (Or (Bot) (mult_disj x0 (Bot)))) <= n). split.
simpl. apply form_enum_index. lia. apply l in H2. exfalso. lia.
Qed.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* List of disjunctions. *)
Lemma Id_list_disj : forall Γ l0 l1,
BIH_rules (Γ, list_disj l0 --> list_disj (l0 ++ l1)).
Proof.
induction l0 ; intros.
- simpl. apply wEFQ.
- simpl. apply wmonotL_Or. apply IHl0.
Qed.
Lemma list_disj_app : forall l0 Γ A l1,
BIH_rules (Γ, A --> list_disj (l0 ++ l1)) -> BIH_rules (Γ, A --> (Or (list_disj l0) (list_disj l1))).
Proof.
induction l0.
- simpl. intros.
apply MP with (ps:=[(Γ, ((list_disj l1) --> Or (Bot) (list_disj l1)) --> (A --> Or (Bot) (list_disj l1)));(Γ, (list_disj l1) --> Or (Bot) (list_disj l1))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> (list_disj l1)) --> ((list_disj l1) --> Or (Bot) (list_disj l1)) --> (A --> Or (Bot) (list_disj l1)));(Γ,A --> (list_disj l1))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists A. exists (list_disj l1). exists (Or (Bot) (list_disj l1)). auto. inversion H2.
2: inversion H3. subst. assumption. inversion H1. 2: inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists (Bot). exists (list_disj l1). auto.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (A --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or a (list_disj (l0 ++ l1))) --> (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (A --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, A --> Or a (list_disj (l0 ++ l1)))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists A. exists (Or a (list_disj (l0 ++ l1))). exists (Or (Or a (list_disj l0)) (list_disj l1)).
auto. inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst.
apply MP with (ps:=[(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or (Or a (list_disj l0)) (list_disj l1)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ, (Or a (list_disj (l0 ++ l1)) --> Or a (Or (list_disj l0) (list_disj l1))) --> (Or a (Or (list_disj l0) (list_disj l1)) --> Or (Or a (list_disj l0)) (list_disj l1)) --> (Or a (list_disj (l0 ++ l1)) --> Or (Or a (list_disj l0)) (list_disj l1)));
(Γ, (Or a (list_disj (l0 ++ l1)) --> Or a (Or (list_disj l0) (list_disj l1))))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Or a (list_disj (l0 ++ l1))). exists (Or a (Or (list_disj l0) (list_disj l1))).
exists (Or (Or a (list_disj l0)) (list_disj l1)). auto. inversion H4. 2: inversion H5.
subst. apply wmonotL_Or. apply IHl0. apply wimp_Id_gen. inversion H3. 2: inversion H4. subst.
remember (list_disj l0) as E. remember (list_disj l1) as F.
apply MP with (ps:=[(Γ, ((Or E F) --> Or (Or a E) F) --> (Or a (Or E F) --> Or (Or a E) F));
(Γ, ((Or E F) --> Or (Or a E) F))]). 2: apply MPRule_I. intros. inversion H4. rewrite <- H5.
apply MP with (ps:=[(Γ, (a --> Or (Or a E) F) --> ((Or E F) --> Or (Or a E) F) --> (Or a (Or E F) --> Or (Or a E) F));
(Γ, (a --> Or (Or a E) F))]). 2: apply MPRule_I. intros. inversion H6. rewrite <- H7.
apply Ax. apply AxRule_I. apply RA4_I. exists a. exists (Or E F). exists (Or (Or a E) F).
auto. inversion H7. 2: inversion H8. rewrite <- H8.
apply MP with (ps:=[(Γ, ((Or a E) --> Or (Or a E) F) --> (a --> Or (Or a E) F));(Γ, ((Or a E) --> Or (Or a E) F))]).
2: apply MPRule_I. intros. inversion H9. rewrite <- H10.
apply MP with (ps:=[(Γ, (a --> (Or a E)) --> ((Or a E) --> Or (Or a E) F) --> (a --> Or (Or a E) F));(Γ, a --> (Or a E))]).
2: apply MPRule_I. intros. inversion H11. rewrite <- H12. apply Ax. apply AxRule_I.
apply RA1_I. exists a. exists (Or a E). exists (Or (Or a E) F). auto.
inversion H12. 2: inversion H13. rewrite <- H13. apply Ax. apply AxRule_I. apply RA2_I.
exists a. exists E. auto. inversion H10. 2: inversion H11. rewrite <- H11. apply Ax.
apply AxRule_I. apply RA2_I. exists (Or a E). exists F. auto. inversion H5. 2: inversion H6.
rewrite <- H6. apply wmonotR_Or. apply Ax. apply AxRule_I. apply RA3_I. exists a. exists E. auto.
Qed.
Lemma list_disj_app0 : forall l0 Γ A l1,
BIH_rules (Γ, A --> (Or (list_disj l0) (list_disj l1))) -> BIH_rules (Γ, A --> list_disj (l0 ++ l1)).
Proof.
induction l0.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or (Bot) (list_disj l1) --> list_disj l1) --> (A --> list_disj l1));
(Γ, Or (Bot) (list_disj l1) --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or (Bot) (list_disj l1)) --> (Or (Bot) (list_disj l1) --> list_disj l1) --> (A --> list_disj l1));
(Γ, A --> Or (Bot) (list_disj l1))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or (Bot) (list_disj l1)).
exists (list_disj l1). auto. inversion H2. 2: inversion H3. subst. auto. inversion H1.
2: inversion H2. subst.
apply MP with (ps:=[(Γ, ((list_disj l1) --> list_disj l1) --> (Or (Bot) (list_disj l1) --> list_disj l1));
(Γ, (list_disj l1) --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ, (Bot --> list_disj l1) --> ((list_disj l1) --> list_disj l1) --> (Or (Bot) (list_disj l1) --> list_disj l1));
(Γ, Bot --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists (Bot). exists (list_disj l1).
exists (list_disj l1). auto. inversion H4. 2: inversion H5. subst. apply wEFQ.
inversion H3. 2: inversion H4. subst. apply wimp_Id_gen.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))) --> (A --> Or a (list_disj (l0 ++ l1))));
(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or (Or a (list_disj l0)) (list_disj l1)) --> (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))) --> (A --> Or a (list_disj (l0 ++ l1))));
(Γ, A --> Or (Or a (list_disj l0)) (list_disj l1))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists A. exists (Or (Or a (list_disj l0)) (list_disj l1)). exists (Or a (list_disj (l0 ++ l1))).
auto. inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst.
apply MP with (ps:=[(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or a (list_disj (l0 ++ l1))) --> (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))));
(Γ, (Or a (Or (list_disj l0) (list_disj l1)) --> Or a (list_disj (l0 ++ l1))))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (Or (list_disj l0) (list_disj l1))) --> (Or a (Or (list_disj l0) (list_disj l1)) --> Or a (list_disj (l0 ++ l1))) --> (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (list_disj (l0 ++ l1))));
(Γ, (Or (Or a (list_disj l0)) (list_disj l1) --> Or a (Or (list_disj l0) (list_disj l1))))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Or (Or a (list_disj l0)) (list_disj l1)).
exists (Or a (Or (list_disj l0) (list_disj l1))). exists (Or a (list_disj (l0 ++ l1))).
auto. inversion H4. 2: inversion H5.
subst. remember (list_disj l0) as E. remember (list_disj l1) as F.
apply MP with (ps:=[(Γ, (F --> Or a (Or E F)) --> (Or (Or a E) F --> Or a (Or E F)));
(Γ, F --> Or a (Or E F))]). 2: apply MPRule_I. intros. inversion H5. rewrite <- H6.
apply MP with (ps:=[(Γ, ((Or a E) --> Or a (Or E F)) --> (F --> Or a (Or E F)) --> (Or (Or a E) F --> Or a (Or E F)));
(Γ, ((Or a E) --> Or a (Or E F)))]). 2: apply MPRule_I. intros. inversion H7. rewrite <- H8.
apply Ax. apply AxRule_I. apply RA4_I. exists (Or a E). exists F. exists (Or a (Or E F)).
auto. inversion H8. 2: inversion H9. rewrite <- H9. apply wmonotL_Or. apply Ax.
apply AxRule_I. apply RA2_I. exists E. exists F. auto. inversion H6. 2: inversion H7.
rewrite <- H7.
apply MP with (ps:=[(Γ, ((Or E F) --> Or a (Or E F)) --> (F --> Or a (Or E F)));(Γ, ((Or E F) --> Or a (Or E F)))]).
2: apply MPRule_I. intros. inversion H8. rewrite <- H9.
apply MP with (ps:=[(Γ, (F --> (Or E F)) --> ((Or E F) --> Or a (Or E F)) --> (F --> Or a (Or E F)));(Γ, F --> (Or E F))]).
2: apply MPRule_I. intros. inversion H10. rewrite <- H11. apply Ax. apply AxRule_I.
apply RA1_I. exists F. exists (Or E F). exists (Or a (Or E F)). auto.
inversion H11. 2: inversion H12. rewrite <- H12. apply Ax. apply AxRule_I. apply RA3_I.
exists E. exists F. auto. inversion H9. 2: inversion H10. rewrite <- H10. apply Ax.
apply AxRule_I. apply RA3_I. exists a. exists (Or E F). auto. inversion H3. 2: inversion H4.
rewrite <- H4. apply wmonotL_Or. apply IHl0. apply wimp_Id_gen.
Qed.
Lemma list_disj_remove_app : forall l0 l1 Γ A,
BIH_rules (Γ, list_disj (l0 ++ remove_list l0 l1) --> Or A (list_disj (l0 ++ remove eq_dec_form A (remove_list l0 l1)))).
Proof.
induction l0.
- simpl. intros. apply remove_disj.
- simpl. intros.
apply MP with (ps:=[(Γ, (Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))) --> (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))));
(Γ,Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1))))))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ, (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))) --> (Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))) --> (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))));
(Γ,(Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))
--> Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I.
exists (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))).
exists (Or a (Or A (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))).
exists (Or A (Or a (list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1)))))). auto.
inversion H1. 2: inversion H2. subst.
{ simpl. apply wmonotL_Or. clear H1. clear H0. clear H.
remember (remove eq_dec_form a (remove_list l0 l1)) as E.
apply MP with (ps:=[(Γ, (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E))) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))) --> (list_disj (l0 ++ E) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))));
(Γ, (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E))) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))))]).
2: apply MPRule_I. intros. inversion H. rewrite <- H0.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))) --> (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E))) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))) --> (list_disj (l0 ++ E) --> Or A (list_disj (l0 ++ remove eq_dec_form A E))));
(Γ, (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))))]).
2: apply MPRule_I. intros. inversion H1. rewrite <- H2. apply Ax. apply AxRule_I.
apply RA1_I. exists (list_disj (l0 ++ E)). exists (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))).
exists (Or A (list_disj (l0 ++ remove eq_dec_form A E))). auto. inversion H2. rewrite <- H3.
{ simpl. apply MP with (ps:=[(Γ, ((Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))) --> (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))));
(Γ, ((Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))))]).
2: apply MPRule_I. intros. inversion H4. rewrite <- H5.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ E) --> (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E))))) --> ((Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))) --> (list_disj (l0 ++ E) --> Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))));
(Γ, (list_disj (l0 ++ E) --> (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E))))))]).
2: apply MPRule_I. intros. inversion H6. rewrite <- H7. apply Ax. apply AxRule_I. apply RA1_I.
exists (list_disj (l0 ++ E)). exists (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))).
exists (Or A (Or (list_disj l0) (list_disj (remove eq_dec_form A E)))). auto.
inversion H7. 2: inversion H8. rewrite <- H8.
{ remember (Or (list_disj l0) (Or A (list_disj (remove eq_dec_form A E)))) as F.
apply MP with (ps:=[(Γ, ((Or (list_disj l0) (list_disj E)) --> F) --> (list_disj (l0 ++ E) --> F));
(Γ, ((Or (list_disj l0) (list_disj E)) --> F))]). 2: apply MPRule_I. intros.
inversion H9. rewrite <- H10.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ E) --> (Or (list_disj l0) (list_disj E))) --> ((Or (list_disj l0) (list_disj E)) --> F) --> (list_disj (l0 ++ E) --> F));
(Γ, list_disj (l0 ++ E) --> (Or (list_disj l0) (list_disj E)))]). 2: apply MPRule_I. intros.
inversion H11. rewrite <- H12. apply Ax. apply AxRule_I. apply RA1_I.
exists (list_disj (l0 ++ E)). exists (Or (list_disj l0) (list_disj E)). exists F. auto.
inversion H12. 2: inversion H13. rewrite <- H13. apply list_disj_app. apply wimp_Id_gen.
inversion H10. 2: inversion H11. rewrite <- H11. clear H11. clear H10.
clear H9. clear H8. clear H7. clear H6. clear H5. clear H0. clear H4.
clear H3. clear H2. clear H1. clear H. rewrite HeqF. apply wmonotL_Or.
apply remove_disj. }
inversion H5. 2: inversion H6. rewrite <- H6. remember (list_disj l0) as D.
remember (list_disj (remove eq_dec_form A E)) as F.
apply MP with (ps:=[(Γ, (Or A F --> Or A (Or D F)) --> (Or D (Or A F) --> Or A (Or D F)));(Γ, (Or A F) --> Or A (Or D F))]).
2: apply MPRule_I. intros. inversion H7. rewrite <- H8.
apply MP with (ps:=[(Γ, (D --> Or A (Or D F)) --> (Or A F --> Or A (Or D F)) --> (Or D (Or A F) --> Or A (Or D F)));(Γ, D --> Or A (Or D F))]).
2: apply MPRule_I. intros. inversion H9. rewrite <- H10. apply Ax. apply AxRule_I.
apply RA4_I. exists D. exists (Or A F). exists (Or A (Or D F)). auto. inversion H10. 2: inversion H11.
rewrite <- H11.
apply MP with (ps:=[(Γ, ((Or D F) --> Or A (Or D F)) --> (D --> Or A (Or D F)));(Γ, ((Or D F) --> Or A (Or D F)))]).
2: apply MPRule_I. intros. inversion H12. rewrite <- H13.
apply MP with (ps:=[(Γ, (D --> (Or D F)) --> ((Or D F) --> Or A (Or D F)) --> (D --> Or A (Or D F)));(Γ, D --> (Or D F))]).
2: apply MPRule_I. intros. inversion H14. rewrite <- H15. apply Ax. apply AxRule_I.
apply RA1_I. exists D. exists (Or D F). exists (Or A (Or D F)). auto. inversion H15.
rewrite <- H16. apply Ax. apply AxRule_I. apply RA2_I. exists D. exists F. auto.
inversion H16. inversion H13. rewrite <- H14. apply Ax. apply AxRule_I. apply RA3_I.
exists A. exists (Or D F). auto. inversion H14. inversion H8. rewrite <- H9.
apply wmonotL_Or. apply Ax. apply AxRule_I. apply RA3_I. exists D. exists F. auto.
inversion H9. }
inversion H3. inversion H0. 2: inversion H1. rewrite <- H1. apply wmonotL_Or. apply list_disj_app0.
apply wimp_Id_gen. }
inversion H0. 2: inversion H1. subst.
remember ((list_disj (l0 ++ remove eq_dec_form A (remove eq_dec_form a (remove_list l0 l1))))) as E.
apply MP with (ps:=[(Γ, ((Or A E) --> Or A (Or a E)) --> (Or a (Or A E) --> Or A (Or a E)));
(Γ, ((Or A E) --> Or A (Or a E)))]). 2: apply MPRule_I. intros. inversion H1. rewrite <- H2.
apply MP with (ps:=[(Γ, (a --> Or A (Or a E)) --> ((Or A E) --> Or A (Or a E)) --> (Or a (Or A E) --> Or A (Or a E)));
(Γ, (a --> Or A (Or a E)))]). 2: apply MPRule_I. intros. inversion H3. rewrite <- H4. clear H4.
clear H2. apply Ax. apply AxRule_I. apply RA4_I. exists a. exists (Or A E).
exists (Or A (Or a E)). auto. inversion H4. 2: inversion H5. rewrite <- H5.
apply MP with (ps:=[(Γ, ((Or a E) --> Or A (Or a E)) --> (a --> Or A (Or a E))); (Γ, ((Or a E) --> Or A (Or a E)))]).
2: apply MPRule_I. intros. inversion H6. rewrite <- H7.
apply MP with (ps:=[(Γ, (a --> (Or a E)) --> ((Or a E) --> Or A (Or a E)) --> (a --> Or A (Or a E))); (Γ, a --> (Or a E))]).
2: apply MPRule_I. intros. inversion H8. rewrite <- H9. apply Ax. apply AxRule_I. apply RA1_I.
exists a. exists (Or a E). exists (Or A (Or a E)). auto. inversion H9.
rewrite <- H10. 2: inversion H10. apply Ax. apply AxRule_I. apply RA2_I.
exists a. exists E. auto. inversion H7. 2: inversion H8. rewrite <- H8.
apply Ax. apply AxRule_I. apply RA3_I. exists A. exists (Or a E). auto.
inversion H2. rewrite <- H3. apply wmonotL_Or. apply Ax. apply AxRule_I.
apply RA3_I. exists a. exists E. auto. inversion H3.
Qed.
Lemma Id_list_disj_remove : forall Γ l0 l1,
BIH_rules (Γ, list_disj l1 --> list_disj (l0 ++ remove_list l0 l1)).
Proof.
induction l0.
- intros. simpl. apply wimp_Id_gen.
- simpl. intros.
apply MP with (ps:=[(Γ, (list_disj (l0 ++ remove_list l0 l1) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (list_disj l1 --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ, list_disj (l0 ++ remove_list l0 l1) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1))))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ, (list_disj l1 --> list_disj (l0 ++ remove_list l0 l1)) --> (list_disj (l0 ++ remove_list l0 l1) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (list_disj l1 --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ,list_disj l1 --> list_disj (l0 ++ remove_list l0 l1))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (list_disj l1). exists (list_disj (l0 ++ remove_list l0 l1)).
exists (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))). auto.
inversion H1. 2: inversion H2. subst. apply IHl0. inversion H0. subst.
clear H. clear H0. apply list_disj_remove_app. inversion H1.
Qed.
Lemma der_list_disj_remove1 : forall Γ A l0 l1,
(BIH_rules (Γ, A --> list_disj l0)) ->
(BIH_rules (Γ, A --> list_disj (l0 ++ remove_list l0 l1))).
Proof.
intros Γ A. induction l0.
- simpl. intros.
apply MP with (ps:=[(Γ, (Bot --> list_disj l1) --> (A --> list_disj l1));
(Γ, Bot --> list_disj l1)]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Bot) --> (Bot --> list_disj l1) --> (A --> list_disj l1));
(Γ, A --> Bot)]). 2: apply MPRule_I. intros. inversion H1. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Bot). exists (list_disj l1).
auto. inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst. apply wEFQ.
- intros. subst. simpl. simpl in H.
apply MP with (ps:=[(Γ, (Or a (list_disj l0) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (A --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ, (Or a (list_disj l0) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> Or a (list_disj l0)) --> (Or a (list_disj l0) --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))) --> (A --> Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))));
(Γ, A --> Or a (list_disj l0))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or a (list_disj l0)).
exists (Or a (list_disj (l0 ++ remove eq_dec_form a (remove_list l0 l1)))). auto.
inversion H2. 2: inversion H3. subst. auto. inversion H1. 2: inversion H2.
subst. clear H0. clear H1. apply wmonotL_Or. apply Id_list_disj.
Qed.
Lemma der_list_disj_remove2 : forall Γ A l0 l1,
(BIH_rules (Γ, A --> list_disj l1)) ->
(BIH_rules (Γ, A --> list_disj (l0 ++ remove_list l0 l1))).
Proof.
intros.
apply MP with (ps:=[(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (A --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (A --> list_disj l1) --> (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (A --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, A --> list_disj l1)]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists A. exists (list_disj l1). exists (list_disj (l0 ++ (remove_list l0 l1))).
auto. inversion H2. 2 : inversion H3. subst. auto. inversion H1. subst. 2: inversion H2.
clear H0. clear H1.
apply MP with (ps:=[(Γ, ((list_disj (l0 ++ (remove_list l0 l1))) --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, (list_disj (l0 ++ (remove_list l0 l1))) --> (list_disj (l0 ++ (remove_list l0 l1))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))) --> ((list_disj (l0 ++ (remove_list l0 l1))) --> (list_disj (l0 ++ (remove_list l0 l1)))) --> (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))));
(Γ, (list_disj l1 --> (list_disj (l0 ++ (remove_list l0 l1)))))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists (list_disj l1). exists ((list_disj (l0 ++ (remove_list l0 l1)))).
exists (list_disj (l0 ++ (remove_list l0 l1))). auto. inversion H2.
2: inversion H3. subst. clear H1. clear H2. clear H0. apply Id_list_disj_remove.
inversion H1. 2: inversion H2. subst. clear H0. clear H1. apply wimp_Id_gen.
Qed.