G4iSLt.G4iSLT_remove_list

Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.

Require Import existsT.

Require Import G4iSLT_calc.

Set Implicit Arguments.

Lemma In_dec : l (a : MPropF) , (In a l) + ((In a l) False).
Proof.
induction l.
- right. intro. destruct H.
- intro . pose (IHl ). destruct s.
  * left. apply in_cons. assumption.
  * destruct (eq_dec_form a ).
    + subst. left. apply in_eq.
    + right. intro. inversion H.
      { apply n. assumption. }
      { apply f. assumption. }
Qed.


(* Let us prove some lemmas about remove. *)

Lemma in_not_touched_remove : l1 (a0 a1 : MPropF),
        In In (remove eq_dec_form ).
Proof.
induction .
- intros. inversion H.
- intros. simpl. destruct (eq_dec_form a).
  * subst. apply . inversion H. exfalso. apply . auto. assumption. assumption.
  * inversion H. subst. apply in_eq. apply in_cons. apply . assumption. assumption.
Qed.


Lemma remove_dist_app {A : Type} (eq_dec : x y : A, {x = y} + {x y}) :
         (a : A) l1 l2, (@remove A eq_dec a ( )) =
                              (@remove A eq_dec a ) (@remove A eq_dec a ).
Proof.
intros a . induction .
- intro . rewrite app_nil_l. simpl. reflexivity.
- intro . simpl. destruct (eq_dec a ).
  * apply .
  * simpl. rewrite . reflexivity.
Qed.


Lemma remove_not_in_anymore : l (A : MPropF),
          (In A (remove eq_dec_form A l)) False.
Proof.
induction l.
- intros. simpl in H. inversion H.
- intros. simpl in H. destruct (eq_dec_form A a). subst. apply IHl in H. assumption.
  inversion H. apply n. symmetry. assumption. apply IHl in . assumption.
Qed.


Lemma in_remove_in_init : l A B,
    In A (remove eq_dec_form B l) In A l.
Proof.
induction l.
- intros. simpl. inversion H.
- intros. destruct (eq_dec_form A a). subst. apply in_eq. apply in_cons.
  pose (IHl A B). apply i. simpl in H. destruct (eq_dec_form B a).
  * subst. assumption.
  * inversion H. exfalso. apply n. symmetry. assumption. assumption.
Qed.


Lemma remove_preserv_NoDup : l (A : MPropF), NoDup l NoDup (remove eq_dec_form A l).
Proof.
induction l.
- intros. simpl. apply NoDup_nil.
- intros. simpl. destruct (eq_dec_form A a).
  * subst. apply IHl. inversion H. assumption.
  * apply NoDup_cons. intro. apply in_remove_in_init in . inversion H. apply . assumption.
    apply IHl. inversion H. assumption.
Qed.


Lemma NoDup_destr_split : l1 l2 (A : MPropF), NoDup ( A :: ) NoDup ( ).
Proof.
induction .
- intros. rewrite app_nil_l. rewrite app_nil_l in H. inversion H. assumption.
- intros. simpl. apply NoDup_cons. intro. inversion H. subst. apply . apply in_app_or in .
  destruct . apply in_or_app. left. assumption. apply in_or_app. right. apply in_cons.
  assumption. simpl in H. inversion H. subst. apply with (A:=A). assumption.
Qed.


Lemma remove_le_length : l (A : MPropF), length (remove eq_dec_form A l) length l.
Proof.
induction l.
- intros. simpl. reflexivity.
- intros. simpl. destruct (eq_dec_form A a).
  * subst. apply le_S. apply IHl.
  * simpl. apply le_n_S. apply IHl.
Qed.


Lemma remove_In_smaller_length : l (A : MPropF),
                                 In A l length (remove eq_dec_form A l) < length l.
Proof.
induction l.
- intros. inversion H.
- intros. simpl. destruct (eq_dec_form A a).
  * subst. unfold lt. apply le_n_S. apply remove_le_length.
  * simpl. rewrite Nat.succ_lt_mono. apply IHl. inversion H. subst. exfalso. apply n. auto.
    assumption.
Qed.


Lemma double_remove {A : Type} (eq_dec : x y : A, {x = y} + {x y}) :
       a l, (@remove A eq_dec a (@remove A eq_dec a l)) = (@remove A eq_dec a l).
Proof.
intros a l. induction l.
- simpl. reflexivity.
- simpl. destruct (eq_dec a ).
  * subst. apply IHl.
  * simpl. destruct (eq_dec a ).
    + exfalso. apply n. assumption.
    + rewrite IHl. reflexivity.
Qed.


Lemma permut_remove {A : Type} (eq_dec : x y : A, {x = y} + {x y}) :
       a0 a1 l, (@remove A eq_dec (@remove A eq_dec l)) =
                      (@remove A eq_dec (@remove A eq_dec l)).
Proof.
intros l. induction l.
- simpl. reflexivity.
- simpl. destruct (eq_dec a).
  * subst. simpl. destruct (eq_dec a).
    + subst. reflexivity.
    + simpl. destruct (eq_dec a a). apply IHl. exfalso. apply . reflexivity.
  * simpl. destruct (eq_dec a).
    + subst. assumption.
    + simpl. destruct (eq_dec a). exfalso. apply n. assumption.
      rewrite IHl. reflexivity.
Qed.


Lemma In_remove_diff : l (A B : MPropF), In A (remove eq_dec_form B l) A B.
Proof.
induction l ; intros.
- intro. simpl in H. assumption.
- simpl in H. destruct (eq_dec_form B a).
  * subst. apply IHl. assumption.
  * inversion H.
    + subst. intro. apply n. symmetry. assumption.
    + apply IHl. assumption.
Qed.


(* Now we define remove_list and prove some lemmas about it. *)

Fixpoint remove_list (l1 l2: list MPropF) : list MPropF :=
match with
  | []
  | :: remove eq_dec_form (remove_list )
end.

Lemma remove_list_of_nil : (l : list MPropF), remove_list l nil = nil.
Proof.
induction l.
- simpl. reflexivity.
- simpl. rewrite IHl. simpl. reflexivity.
Qed.


Lemma app_remove_list : (l1 l2 l3 : list MPropF),
        remove_list ( ) = remove_list (remove_list ).
Proof.
induction .
- simpl. firstorder.
- induction .
  * intro . rewrite app_nil_r. simpl. reflexivity.
  * intro . simpl. pose ( ( :: ) ). simpl in e.
    rewrite e. reflexivity.
Qed.


Lemma remove_list_preserv_NoDup : l1 l2, NoDup NoDup (remove_list ).
Proof.
induction .
- intros. simpl. assumption.
- intros. simpl. apply in H. apply remove_preserv_NoDup with (A:=a) in H.
  assumption.
Qed.


Lemma remove_list_cont : l1 A, In A ( l2, In A (remove_list ) False).
Proof.
induction .
- intros. inversion H.
- intros. inversion H.
  * subst. simpl in . apply remove_not_in_anymore in . assumption.
  * simpl in . pose ( A ). apply f. apply in_remove_in_init with (B:= a). assumption.
Qed.


Lemma remove_list_dist_app : (l1 l2 l3 : list MPropF),
        remove_list ( ) = (remove_list ) (remove_list ).
Proof.
induction .
- intros. simpl. reflexivity.
- simpl. intros. rewrite . simpl. rewrite remove_dist_app. reflexivity.
Qed.


Lemma permut_remove_remove_list : a (l1 l2 : list MPropF),
      remove eq_dec_form a (remove_list ) =
      remove_list (remove eq_dec_form a ).
Proof.
intros a . generalize dependent a. induction ; simpl.
- reflexivity.
- intros. rewrite permut_remove. rewrite . reflexivity.
Qed.


Lemma swap_remove_list : (l1 l2 l3 : list MPropF),
      remove_list ( ) = remove_list ( ) .
Proof.
induction .
- intros. rewrite app_nil_l. rewrite app_nil_r. reflexivity.
- induction .
  * rewrite app_nil_l. rewrite app_nil_r. reflexivity.
  * intro . simpl. rewrite . simpl. rewrite permut_remove.
    rewrite . simpl. rewrite . reflexivity.
Qed.


Lemma redund_remove_remove_list : a (l1 l2 : list MPropF),
      remove eq_dec_form a (remove_list (remove eq_dec_form a ) ) =
      remove eq_dec_form a (remove_list ).
Proof.
intro a. induction .
- intro . simpl. reflexivity.
- intro . simpl. destruct (eq_dec_form a ).
  * rewrite . subst. rewrite double_remove. reflexivity.
  * simpl. rewrite permut_remove. rewrite . apply permut_remove.
Qed.


Lemma redund_remove : (l1 l2 l3 : list MPropF) a,
      remove eq_dec_form a (remove_list (remove_list (remove eq_dec_form a ) )) =
      remove eq_dec_form a (remove_list (remove_list )).
Proof.
intros. repeat rewrite app_remove_list. rewrite swap_remove_list.
rewrite app_remove_list. rewrite redund_remove_remove_list. rewrite app_remove_list.
rewrite swap_remove_list. reflexivity.
Qed.


Lemma redund_remove_list : (l1 l2 l3 : list MPropF),
      remove_list (remove_list (remove_list ) ) = remove_list (remove_list ).
Proof.
induction ; intros ; simpl.
- reflexivity.
- rewrite redund_remove. rewrite . reflexivity.
Qed.


Lemma remove_list_in_single : l1 a, (In a ) remove_list [a] = nil.
Proof.
induction .
- intros. inversion H.
- intros. inversion H.
  * subst. simpl. rewrite permut_remove_remove_list. simpl. destruct (eq_dec_form ).
    apply remove_list_of_nil. exfalso. apply n. reflexivity.
  * apply in . simpl. rewrite . simpl. reflexivity.
Qed.


Lemma not_removed_remove_list : l2 l1 A, In A (In A False) In A (remove_list ).
Proof.
induction .
- intros. inversion H.
- induction .
  * intros. simpl. assumption.
  * intros. simpl. pose (in_not_touched_remove (remove_list (a :: ))). pose (i A).
    pose ( ). apply . apply . assumption. intro. apply . apply in_cons. assumption.
    clear . clear . clear i. destruct (eq_dec_form A ). intro. apply . subst. apply in_eq.
    assumption.
Qed.


Lemma add_remove_list_preserve_NoDup : (l1 l2 : list MPropF),
            NoDup NoDup NoDup ( (remove_list )).
Proof.
induction .
- intros. rewrite app_nil_l. simpl. assumption.
- intros. simpl. apply NoDup_cons.
  * intro. apply in_app_or in . destruct . inversion H. apply . assumption.
    apply remove_not_in_anymore in . assumption.
  * rewrite permut_remove_remove_list. apply . inversion H. assumption.
    apply remove_preserv_NoDup. assumption.
Qed.


Lemma remove_list_is_in : l1 l2 A, In A In A ( (remove_list )).
Proof.
intros. pose (In_dec A). destruct s.
- apply in_or_app. left. assumption.
- apply in_or_app. right. apply not_removed_remove_list ; assumption.
Qed.


Lemma In_remove_same : l1 l2 (A : MPropF), In A
                remove_list (A :: ) = remove_list .
Proof.
induction .
- intros. inversion H.
- intros. inversion H.
  * subst. simpl. rewrite permut_remove_remove_list. simpl. destruct (eq_dec_form A A).
    rewrite permut_remove_remove_list. reflexivity. exfalso. apply n. reflexivity.
  * simpl. pose ( A ). rewrite e. reflexivity.
Qed.


Lemma In_remove_length_same : l1 l2 (A : MPropF), In A
                length (remove_list (A :: )) = length (remove_list ).
Proof.
intros. rewrite In_remove_same. reflexivity. assumption.
Qed.


Lemma length_le_remove_list : (l1 l2 : list MPropF), length (remove_list ) length .
Proof.
induction .
- intros. auto.
- intros. simpl. rewrite permut_remove_remove_list. pose ( (remove eq_dec_form a )).
  apply Nat.le_trans with (m:=length (remove eq_dec_form a )). assumption.
  apply remove_le_length.
Qed.


Lemma remove_list_singl_id_or_nil : l (A : MPropF), remove_list l [A] = nil remove_list l [A] = [A].
Proof.
induction l.
- intros. right. auto.
- intros. pose (IHl A). destruct o. left. simpl. rewrite H. auto.
  simpl. rewrite H. destruct (eq_dec_form A a).
  * subst. left. simpl. destruct (eq_dec_form a a). reflexivity. exfalso. apply n.
    reflexivity.
  * right. simpl. destruct (eq_dec_form a A). exfalso. apply n. symmetry. assumption.
    reflexivity.
Qed.


Lemma remove_list_non_empty_inter_smaller_length : l2 l1 (A : MPropF),
                                 In A In A length (remove_list ) < length .
Proof.
induction .
- intros. inversion .
- intros. simpl. destruct (eq_dec_form A a).
  * subst. rewrite In_remove_length_same. 2: assumption. unfold lt. apply le_n_S.
    apply length_le_remove_list.
  * inversion .
    + exfalso. apply n. symmetry. assumption.
    + assert (a :: = [a] ). auto. rewrite . rewrite remove_list_dist_app.
      rewrite app_length. pose (remove_list_singl_id_or_nil a). destruct o.
      rewrite . simpl. apply Nat.lt_lt_succ_r. apply with (A:=A) ; assumption.
      rewrite . simpl. rewrite Nat.succ_lt_mono. apply with (A:=A) ; assumption.
Qed.


Lemma remove_list_delete_head : l1 l2 l3 A, remove_list ( A :: ) (A :: ) = remove_list ( A :: ) .
Proof.
induction ; intros ; simpl.
- rewrite permut_remove_remove_list. simpl. destruct (eq_dec_form A A). symmetry. apply permut_remove_remove_list.
  exfalso. apply n. reflexivity.
- rewrite . reflexivity.
Qed.


Lemma remove_list_delete_head_In : l1 l2 A, In A remove_list (A :: ) = remove_list .
Proof.
intros. pose (In_split A H). destruct e. destruct . subst. apply remove_list_delete_head.
Qed.


Lemma remove_list_in_nil : l1 l2 l3 A,
        remove_list ( A :: ) = nil
        ( l4 l5, = A :: ).
Proof.
induction .
- intros. simpl in H. destruct ; inversion H.
- induction .
  * intros. simpl in H. rewrite permut_remove_remove_list in H. simpl in H. destruct (eq_dec_form a A).
    + subst. exists []. exists . auto.
    + pose ( [] (remove eq_dec_form a )). simpl in s. apply s in H. destruct H. destruct .
      exists ([a] x). exists . subst. auto.
  * intros. simpl in H. rewrite permut_remove_remove_list in H. simpl in H. destruct (eq_dec_form a ).
    + subst. pose ( A). apply s. rewrite permut_remove_remove_list in H. simpl. assumption.
    + pose ( [] (remove eq_dec_form a ( A :: )) ). pose (s H). repeat destruct .
      subst. apply with (:= ). simpl. rewrite permut_remove_remove_list.
      rewrite remove_list_delete_head in H. assumption.
Qed.


Lemma remove_list_is_nil : l1 l2, (remove_list = nil ( A, (In A ) (In A ))).
Proof.
induction .
- intro . split.
  * intros. simpl in H. rewrite H. assumption.
  * intros. simpl. destruct .
    + reflexivity.
    + exfalso. pose (H m). assert (In m (m :: )). apply in_eq. apply i in . inversion .
- induction .
  * split.
    + intros. inversion .
    + intros. apply remove_list_of_nil.
  * split.
    + intros. simpl in H. rewrite permut_remove_remove_list in H. simpl in H. destruct (eq_dec_form a ).
      subst. inversion . subst. apply in_eq. rewrite permut_remove_remove_list in H. simpl in .
      rewrite in H. apply H in . destruct . subst. apply in_eq. apply in_cons. assumption.
      inversion . subst. apply in_cons. pose (remove_list_in_nil [] (remove eq_dec_form a ) A).
      simpl in s. apply s in H. destruct H. destruct . subst. apply in_or_app. right. apply in_eq.
      apply . 2: assumption. simpl. rewrite permut_remove_remove_list.
      pose (app_eq_nil (remove_list []) (remove_list (remove eq_dec_form a ))). simpl in .
      assert (: remove_list [] remove_list (remove eq_dec_form a ) = []).
      rewrite remove_list_dist_app. simpl. assumption. apply in . destruct . assumption.
    + intros. simpl. rewrite permut_remove_remove_list. simpl. destruct (eq_dec_form a ).
      { subst. rewrite permut_remove_remove_list. simpl in . rewrite . intros.
        pose (H A). apply i. apply in_cons. assumption. }
      { assert (: ( A : MPropF, In A In A (a :: ))). intros. apply H.
        apply in_cons. assumption. apply in .
        assert (: :: remove eq_dec_form a = [] remove eq_dec_form a ). auto.
        rewrite . rewrite remove_list_dist_app. clear . rewrite permut_remove_remove_list.
        simpl in . rewrite . rewrite app_nil_r. apply remove_list_in_single. pose (H ).
        assert (: In ( :: )). apply in_eq. apply i in . inversion . exfalso. apply n.
        assumption. assumption. }
Qed.


Lemma remove_delete_origin : l1 l2 (A B : MPropF), (A B)
            length (remove eq_dec_form A ( B :: )) = S (length (remove eq_dec_form A ( ))).
Proof.
induction .
- intros. repeat rewrite app_nil_l. simpl. destruct (eq_dec_form A B). exfalso. apply H. assumption.
  simpl. reflexivity.
- intros. simpl. destruct (eq_dec_form A a).
  * apply . assumption.
  * simpl. apply eq_S. apply . assumption.
Qed.


Lemma keep_list_delete_head_not_origin : l1 l2 l3 A, ((In A ) False)
                length (remove_list ( A :: )) = S (length (remove_list ( ))).
Proof.
induction .
- intros. simpl. rewrite app_length. simpl. rewrite app_length. auto.
- intros. simpl. repeat rewrite remove_list_dist_app. assert (In A False).
  intro. apply H. apply in_cons. assumption. assert (A :: = [A] ).
  auto. rewrite . rewrite remove_list_dist_app. pose (remove_list_singl_id_or_nil A).
  destruct o. exfalso. rewrite remove_list_is_nil in . apply . apply .
  apply in_eq. rewrite . apply remove_delete_origin. intro. apply H. subst. apply in_eq.
Qed.


Lemma keep_list_delete_head_not_In : l1 l2 A, ((In A ) False)
                length (remove_list (A :: )) = S (length (remove_list )).
Proof.
intros. pose (@keep_list_delete_head_not_origin [] A H). repeat rewrite app_nil_l in e.
assumption.
Qed.


Lemma In_remove_In_list : (A B : MPropF) l, In A (remove eq_dec_form B l) In A l.
Proof.
induction l ; intros.
- simpl in H. destruct H.
- simpl in H. destruct (eq_dec_form B a).
  * subst. apply in_cons. apply IHl. assumption.
  * inversion H.
    + subst. apply in_eq.
    + apply in_cons. apply IHl. assumption.
Qed.


Lemma In_remove_list_In_list : (A : MPropF) l1 l2, In A (remove_list ) In A .
Proof.
intro A. induction ; intros.
- simpl in H. assumption.
- simpl in H. apply In_remove_In_list in H. apply . assumption.
Qed.


Lemma In_remove_list_In_list_not_In_remove_list : (A : MPropF) l1 l2,
            In A (remove_list ) (In A ((In A ) False)).
Proof.
intro A. induction ; intros.
- simpl in H. split. assumption. intro. inversion .
- simpl in H. split. apply In_remove_In_list in H. apply . assumption. intro.
  inversion .
  * subst. apply remove_not_in_anymore in H. assumption.
  * apply In_remove_In_list in H. apply in H. destruct H. apply . assumption.
Qed.


Lemma remove_list_incr_decr3 : (l3 l2 l1 : list MPropF),
              (incl )
              length (remove_list ) length (remove_list ).
Proof.
induction ; intros.
- repeat rewrite remove_list_of_nil. auto.
- destruct (In_dec a).
  + rewrite remove_list_delete_head_In. 2: assumption. destruct (In_dec a).
    * rewrite remove_list_delete_head_In. 2: assumption. apply ; auto.
    * rewrite keep_list_delete_head_not_In. 2: assumption. apply Nat.le_le_succ_r.
      apply . assumption.
  + repeat rewrite keep_list_delete_head_not_In. apply le_n_S. apply ; auto.
    intro. apply f. apply H. assumption. assumption.
Qed.


Lemma remove_list_incr_decr1 : (l3 l1 l2: list MPropF),
              ( A, In A In A (In A False))
              (incl )
              length (remove_list ) < length (remove_list ).
Proof.
induction .
- intros. destruct H. destruct H. destruct . exfalso. inversion .
- intros. destruct H. destruct H. destruct . destruct (eq_dec_form a x).
  * subst. rewrite remove_list_delete_head_In. 2: assumption.
    rewrite keep_list_delete_head_not_In. 2: assumption. unfold lt.
    apply le_n_S. apply remove_list_incr_decr3. assumption.
  * inversion . exfalso. apply n ; assumption.
    assert (: A : MPropF, In A In A (In A False)).
    exists x. auto. apply in . 2 : assumption. unfold lt.
    destruct (In_dec a).
    + rewrite remove_list_delete_head_In. 2: assumption. destruct (In_dec a).
      { rewrite remove_list_delete_head_In. 2: assumption. apply . }
      { rewrite keep_list_delete_head_not_In. 2: assumption. apply le_n_S.
        unfold lt in . apply Nat.lt_le_incl. assumption. }
    + rewrite keep_list_delete_head_not_In. 2: assumption. rewrite keep_list_delete_head_not_In.
      unfold lt in . apply le_n_S. assumption. intro. apply f. apply . assumption.
Qed.


Lemma remove_list_incr_decr2 : (l4 l3 l1 : list MPropF),
              (NoDup )
              (NoDup )
              (incl )
              length (remove_list ) length (remove_list ).
Proof.
induction .
- intros. rewrite remove_list_of_nil. simpl. apply le_0_n.
- intros. destruct (In_dec a).
  * rewrite remove_list_delete_head_In. 2: assumption. apply ; try assumption.
    inversion H. assumption. unfold incl. intros. apply . apply in_cons. assumption.
  * rewrite keep_list_delete_head_not_In. 2: assumption. assert (: In a ). apply .
    apply in_eq. pose (in_split a ). repeat destruct e. destruct . rewrite .
    rewrite keep_list_delete_head_not_origin. 2: assumption. apply le_n_S. apply .
    inversion H. assumption. subst. apply NoDup_destr_split with (A:=a). assumption.
    inversion H. unfold incl. intros. subst. assert ( : In (a :: )). apply in_cons.
    assumption. pose ( ). apply in_app_or in i. destruct i. apply in_or_app. left.
    assumption. inversion . subst. exfalso. apply . assumption. apply in_or_app. right.
    assumption.
Qed.


Lemma remove_list_incr_decr4 : (l4 l3 l1: list MPropF),
              (NoDup )
              (NoDup )
              (incl )
              ((incl ) False)
              ( A, (In A ) ((In A ) False) ((In A ) False))
              length (remove_list ) < length (remove_list ).
Proof.
induction .
- intros. rewrite remove_list_of_nil. simpl. destruct . destruct . destruct . pose (In_split x ).
  destruct e. destruct . subst. rewrite keep_list_delete_head_not_origin. 2: assumption.
  apply Nat.lt_0_succ.
- intros. destruct (In_dec a).
  * rewrite remove_list_delete_head_In. 2: assumption. apply ; try assumption.
    inversion H. assumption. unfold incl. intros. apply . apply in_cons. assumption.
    intro. apply . unfold incl. intros. apply in_cons. apply . assumption. destruct .
    destruct . destruct . exists x. repeat split ; try assumption. intro. apply .
    apply in_cons. assumption.
  * rewrite keep_list_delete_head_not_In. 2: assumption. assert (In a ). apply .
    apply in_eq. pose (In_split a ). destruct e. destruct . subst.
    rewrite keep_list_delete_head_not_origin. 2 : assumption. rewrite Nat.succ_lt_mono.
    apply . inversion H. assumption. apply NoDup_destr_split with (A:=a). assumption.
    unfold incl. intros. pose ( ). assert (In (a :: )). apply in_cons. assumption.
    apply i in . apply in_app_or in . destruct . apply in_or_app. left. assumption.
    inversion . subst. inversion H. exfalso. apply . assumption. apply in_or_app. right.
    assumption. intro. apply . unfold incl. intros. apply in_app_or in . destruct .
    apply in_cons. apply . apply in_or_app. left. assumption. inversion . subst. apply in_eq.
    apply in_cons. apply . apply in_or_app. right. assumption.
    destruct . destruct . destruct . exists . repeat split ; try assumption.
    apply in_app_or in . destruct . apply in_or_app. left. assumption. inversion .
    subst. exfalso. apply . apply in_eq. apply in_or_app. right. assumption.
    intro. apply . apply in_cons. assumption.
Qed.


Lemma remove_list_incr_decr : (l1 l2 l3 l4 : list MPropF),
              (NoDup )
              (NoDup )
              ( A, In A In A (In A False))
              (incl )
              (incl )
              length (remove_list ) < length (remove_list ).
Proof.
intros. unfold lt.
pose (remove_list_incr_decr2 H ).
repeat destruct . destruct . destruct (In_dec x).
- assert (: ( A, In A In A (In A False))).
  exists x. repeat split ; assumption. pose (@remove_list_incr_decr1 ).
  unfold lt in . apply Nat.le_trans with (m:=length (remove_list )) ; assumption.
- assert ((incl ) False). intros. apply f. apply . assumption.
  assert (( A, (In A ) ((In A ) False) ((In A ) False))). exists x. auto.
  pose (@remove_list_incr_decr3 ). pose (@remove_list_incr_decr4 H ).
  unfold lt in . apply le_n_S in . lia.
Qed.


Lemma In_remove_list_remove_redund : l1 l2 a, In a
                remove eq_dec_form a (remove_list ) = remove_list .
Proof.
induction .
- intros. inversion H.
- intros. simpl. inversion H.
  * subst. rewrite double_remove. reflexivity.
  * pose ( ). rewrite permut_remove. rewrite e. reflexivity.
Qed.


Lemma In_matters_remove_list : l1 l2, (incl incl ) ( l0,
                                    remove_list = remove_list ).
Proof.
induction .
- intros. destruct H. destruct . auto. unfold incl in . pose ( m). assert (In m (m :: )).
  apply in_eq. apply i in . inversion .
- intros. destruct H. simpl. pose (H a). assert (In a (a :: )). apply in_eq. apply i in .
  apply in_split in . destruct . destruct . subst. destruct (In_dec a).
  * rewrite In_remove_list_remove_redund. 2: assumption. apply . split. intro. intro.
    apply H. apply in_cons. assumption. intro. intro. apply in . inversion . subst.
    assumption. assumption.
  * rewrite swap_remove_list. simpl. rewrite redund_remove_remove_list with (:=( x)).
    pose ( (remove eq_dec_form a ( x))). rewrite e.
    auto. split. intro. intro. apply in_not_touched_remove. assert (In (a :: )). apply in_cons.
    assumption. apply H in . apply in_app_or in . destruct . apply in_or_app. right. assumption.
    inversion . subst. exfalso. apply f. assumption. apply in_or_app. left. assumption.
    intro. subst. apply f. assumption. intro. intro. pose (In_remove_diff ( x) ).
    pose (In_remove_In_list a ( x) ). assert (In (x a :: )). apply in_app_or in .
    destruct . apply in_or_app. right. apply in_cons. assumption. apply in_or_app. left. assumption.
    apply in . inversion . exfalso. apply n. symmetry. assumption. assumption.
Qed.