Require Export List.

Definition all_equiv (l: list Prop) :=
  forall x y, In x l -> In y l -> (x <-> y).

Lemma all_equiv_chara : forall l,
  all_equiv l <-> forall x y, In x l -> In y l -> x -> y.
Proof.
(* Goal: forall (l1 l2 : list Prop) (_ : @incl Prop l1 l2) (_ : all_equiv l2), all_equiv l1 *)
  unfold all_equiv.
(* Goal: forall l : list Prop, iff (forall (x y : Prop) (_ : @In Prop x l) (_ : @In Prop y l), iff x y) (forall (x y : Prop) (_ : @In Prop x l) (_ : @In Prop y l) (_ : x), y) *)
  intro l; split; [intros He x y Hx Hy; rewrite (He x y); auto|].
(* Goal: forall (_ : forall (x y : Prop) (_ : @In Prop x l) (_ : @In Prop y l) (_ : x), y) (x y : Prop) (_ : @In Prop x l) (_ : @In Prop y l), iff x y *)
  intros Himp x y Hxl Hyl.
(* Goal: iff x y *)
  split; apply Himp; assumption.
Qed.

Definition all_equiv'_aux (l: list Prop) : Prop.
(* Goal: Prop *)
induction l; [exact True|].
(* Goal: Prop *)
induction l; [exact True|].
(* Goal: Prop *)
exact ((a -> a0) /\ IHl).
Defined.

Lemma all_equiv'_auxP : forall l n1 n2 d1 d2,
  l <> nil -> all_equiv'_aux l ->
  n1 < length l -> n2 < length l -> n1 <= n2 ->
  nth n1 l d1 -> nth n2 l d2.
Proof.
intro l; elim l; [intros ? ? ? ? H; exfalso; apply H; auto|
                  clear l; intros a l _; revert a].
(* Goal: forall (a : Prop) (n1 n2 : nat) (d1 d2 : Prop) (_ : not (@eq (list Prop) (@cons Prop a l) (@nil Prop))) (_ : all_equiv'_aux (@cons Prop a l)) (_ : lt n1 (@length Prop (@cons Prop a l))) (_ : lt n2 (@length Prop (@cons Prop a l))) (_ : le n1 n2) (_ : @nth Prop n1 (@cons Prop a l) d1), @nth Prop n2 (@cons Prop a l) d2 *)
elim l; [intro a|clear l; intros b l IHl a]; intros n1 n2 d1 d2 _ H Hn1 Hn2 Hn.

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
(* Goal: forall _ : @nth Prop n1 (@cons Prop a (@nil Prop)) d1, @nth Prop n2 (@cons Prop a (@nil Prop)) d2 *)
  simpl in Hn1, Hn2.
(* Goal: forall _ : @nth Prop n1 (@cons Prop a (@nil Prop)) d1, @nth Prop n2 (@cons Prop a (@nil Prop)) d2 *)
  apply PeanoNat.Nat.lt_1_r in Hn1; rewrite Hn1.
(* Goal: forall _ : @nth Prop O (@cons Prop a (@nil Prop)) d1, @nth Prop n2 (@cons Prop a (@nil Prop)) d2 *)
  apply PeanoNat.Nat.lt_1_r in Hn2; rewrite Hn2; simpl; auto.
  }

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
(* Goal: forall _ : @nth Prop n1 (@cons Prop a (@cons Prop b l)) d1, @nth Prop n2 (@cons Prop a (@cons Prop b l)) d2 *)
  destruct H as [HI H]. revert dependent n2. revert dependent n1; intro n1.
(* Goal: forall (_ : lt n1 (@length Prop (@cons Prop a (@cons Prop b l)))) (n2 : nat) (_ : lt n2 (@length Prop (@cons Prop a (@cons Prop b l)))) (_ : le n1 n2) (_ : @nth Prop n1 (@cons Prop a (@cons Prop b l)) d1), @nth Prop n2 (@cons Prop a (@cons Prop b l)) d2 *)
  elim n1; [|clear n1; intros n1 IHn1]; intro Hn1.

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
    {
(* Goal: forall (n2 : nat) (_ : lt n2 (@length Prop (@cons Prop a (@cons Prop b l)))) (_ : le O n2) (_ : @nth Prop O (@cons Prop a (@cons Prop b l)) d1), @nth Prop n2 (@cons Prop a (@cons Prop b l)) d2 *)
    intro n2; elim n2; [simpl; auto|clear n2; intros n2 IHn2 Hn2 _ Ha].
    simpl in Ha; apply HI in Ha; apply IHl with 0 d1; auto; simpl in *;
    [discriminate|apply PeanoNat.Nat.lt_0_succ|
     apply Lt.lt_S_n; auto|apply le_0_n].
    }

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
    {
    intro n2; elim n2;
    [intros _ HF; apply PeanoNat.Nat.nle_succ_0 in HF; intuition|
     clear n2; intros n2 IHn2 Hn2 HLe H'].
    assert (Hnth : forall n (l : list Prop) a d,
                     nth (S n) (a :: l) d = nth n l d)
      by (intro n; induction n; simpl; auto).
    rewrite Hnth; rewrite Hnth in H'; clear Hnth; apply IHl with n1 d1; auto;
    [discriminate|simpl in Hn1|simpl in Hn2|apply Le.le_S_n]; auto;
(* Goal: forall _ : x, z *)
    apply Lt.lt_S_n; auto.
    }
  }
Qed.

Definition all_equiv' (l: list Prop) : Prop.
(* Goal: Prop *)
induction l; [exact True|].
(* Goal: Prop *)
exact ((last l a -> a) /\ all_equiv'_aux (a::l)).
Defined.
(*
Definition all_equiv' (l: list Prop) : Prop.
Proof.
(* Goal: Prop *)
induction l; [exact True|].
(* Goal: Prop *)
induction l; [exact True|].
exact ((a <-> a0) /\ IHl).
Defined.

Lemma all_equiv_equiv : forall l, all_equiv l <-> all_equiv' l.
Proof.
assert (IH : forall a a0 l,
  all_equiv' (a::a0::l) <-> (a <-> a0) /\ all_equiv' (a0::l))
  by (intros a a0 l; induction l; simpl; tauto).
unfold all_equiv; intro l; induction l; [simpl; tauto|].
induction l; [simpl|clear IHl0; rewrite IH; split]; clear IH.

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
  split; [auto|intros _ x y Hx Hy].
  elim Hx; [clear Hx; intro Hx; rewrite <- Hx|intuition].
(* Goal: forall _ : x, z *)
(* Goal: forall _ : x, z *)
  elim Hy; [clear Hy; intro Hy; rewrite <- Hy|]; intuition.
  }

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
  intro H; split; [apply H; simpl; tauto|].
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
  apply IHl; intros x y Hx Hy; apply H; right; assumption.
  }

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
  intros [H Hl] x y [Ha|Hx] [Ha'|Hy];
  try (rewrite <- Ha; clear Ha);
  try (rewrite <- Ha'; clear Ha'); [tauto| | |];
  try (cut (a0 <-> y); [try tauto|apply IHl; try assumption; left; reflexivity]);
  try (cut (a0 <-> x); [tauto|apply IHl; try assumption; left; reflexivity]).
  }
Qed.
*)

Lemma all_equiv__equiv : forall l, all_equiv l <-> all_equiv' l.
Proof.
(* Goal: forall l : list Prop, iff (all_equiv l) (all_equiv' l) *)
intro l; split.

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
(* Goal: forall _ : all_equiv l, all_equiv' l *)
  elim l; [simpl; auto|clear l; intros a l _; revert a].
(* Goal: forall (a : Prop) (_ : all_equiv (@cons Prop a l)), all_equiv' (@cons Prop a l) *)
  elim l; [simpl; intros; split; auto|clear l; intros b l _ a H; split].

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
    {
(* Goal: forall _ : @last Prop (@cons Prop b l) a, a *)
    apply H; [apply in_eq|clear H; apply in_cons; revert b; revert a].
(* Goal: forall a b : Prop, @In Prop (@last Prop (@cons Prop b l) a) (@cons Prop b l) *)
    elim l; [simpl; auto|clear l; intros b l IHl d a].
    assert (H : last (a :: b :: l) = last (b :: l))
(* Goal: forall _ : x, z *)
      by (induction l; simpl; auto); rewrite H; apply in_cons; auto.
    }

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
    {
    revert H; revert b; revert a; elim l; [|clear l; intros c l IHl a b H];
    [simpl; intros a b H; split; auto; apply H; [apply in_cons|]; apply in_eq|].
(* Goal: all_equiv'_aux (@cons Prop a (@cons Prop b (@cons Prop c l))) *)
    split; [apply H; [apply in_cons|]; apply in_eq|].
(* Goal: all_equiv'_aux (@cons Prop b (@cons Prop c l)) *)
    apply IHl; intros x y Hx Hy; apply H; apply in_cons; auto.
    }
  }

(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
  {
(* Goal: forall _ : all_equiv' l, all_equiv l *)
  elim l; [unfold all_equiv; simpl; tauto|clear l; intros a l _; revert a].
  elim l;[ unfold all_equiv; simpl; intros a _ x y Hx Hy;
           elim Hx; [clear Hx; intro Hx|tauto];
           elim Hy; [clear Hy; intro Hy|tauto];
           rewrite <- Hx; rewrite Hy; tauto|clear l; intros b l _ a H].
(* Goal: all_equiv (@cons Prop a (@cons Prop b l)) *)
  intros x y Hx Hy; destruct H as [Hend Hbeg].
(* Goal: iff x y *)
  destruct (In_nth _ _ a Hx) as [n1 Hn1]; clear Hx; destruct Hn1 as [Hn1 Hx].
(* Goal: iff x y *)
  destruct (In_nth _ _ a Hy) as [n2 Hn2]; clear Hy; destruct Hn2 as [Hn2 Hy].
(* Goal: iff x y *)
  assert (Hlast : nth (S (length l)) (a :: b :: l) a = last (b :: l) a).
(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
(* Goal: iff x y *)
    {
(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) a) (@last Prop (@cons Prop b l) a) *)
    transitivity (nth (length l) (b :: l) a); [simpl; auto|].
(* Goal: @eq Prop (@nth Prop (@length Prop l) (@cons Prop b l) a) (@last Prop (@cons Prop b l) a) *)
    revert dependent b. intros b _ _ _ _ _ _; clear n1 n2 x y.
(* Goal: forall a b : Prop, @In Prop (@last Prop (@cons Prop b l) a) (@cons Prop b l) *)
    revert b; revert a; elim l; [simpl; auto|clear l; intros b l IHl d a].
(* Goal: @eq Prop (@nth Prop (@length Prop (@cons Prop b l)) (@cons Prop a (@cons Prop b l)) d) (@last Prop (@cons Prop a (@cons Prop b l)) d) *)
    transitivity (nth (S (length l)) (a :: b :: l) d); [simpl; auto|].
(* Goal: @eq Prop (@nth Prop (S (@length Prop l)) (@cons Prop a (@cons Prop b l)) d) (@last Prop (@cons Prop a (@cons Prop b l)) d) *)
    transitivity (nth (length l) (b :: l) d); [simpl; auto|].
(* Goal: @eq Prop (@nth Prop (@length Prop l) (@cons Prop b l) d) (@last Prop (@cons Prop a (@cons Prop b l)) d) *)
    rewrite IHl; simpl; auto.
    }
(* Goal: iff x y *)
  assert (HaE : a = nth 0 (a :: b :: l) a) by (simpl; auto).
(* Goal: iff x y *)
  rewrite <- Hlast in Hend; clear Hlast; rewrite <- Hx; rewrite <- Hy.
  elim (PeanoNat.Nat.lt_ge_cases n1 n2); intro HLe; split;
  try solve[apply all_equiv'_auxP; auto;
            try apply PeanoNat.Nat.lt_le_incl; auto; discriminate];
  intro H; cut a; try (intro Ha; rewrite HaE in Ha; revert Ha);
  try(apply Hend; revert H); apply all_equiv'_auxP; auto; try discriminate;
  try apply PeanoNat.Nat.le_0_l; simpl in *; try apply PeanoNat.Nat.lt_0_succ;
(* Goal: forall _ : x, z *)
  apply PeanoNat.Nat.lt_succ_r; auto.
  }
Qed.

Definition stronger (l1 l2 : list Prop) :=
  forall x y, In x l1 -> In y l2 -> (x -> y).

Definition all_equiv_under (l1 l2 : list Prop) :=
  forall x y z, In x l1 -> In y l2 -> In z l2 -> (x -> (y <-> z)).

Lemma all_equiv_under_chara : forall l1 l2,
  all_equiv_under l1 l2 <-> forall x, In x l1 -> x -> all_equiv l2.
Proof.
(* Goal: forall l1 l2 : list Prop, iff (all_equiv_under l1 l2) (forall (x : Prop) (_ : @In Prop x l1) (_ : x), all_equiv l2) *)
  unfold all_equiv_under, all_equiv.
(* Goal: forall l1 l2 : list Prop, iff (forall (x y z : Prop) (_ : @In Prop x l1) (_ : @In Prop y l2) (_ : @In Prop z l2) (_ : x), iff y z) (forall (x : Prop) (_ : @In Prop x l1) (_ : x) (x0 y : Prop) (_ : @In Prop x0 l2) (_ : @In Prop y l2), iff x0 y) *)
  intros; split; intros; eauto.
Qed.

Lemma all_equiv2_impl__stronger : forall l1 l2 x y,
  all_equiv l1 -> all_equiv l2 -> In x l1 -> In y l2 -> (x -> y) -> stronger l1 l2.
Proof.
(* Goal: forall (l1 l2 : list Prop) (x y : Prop) (_ : all_equiv l1) (_ : all_equiv l2) (_ : @In Prop x l1) (_ : @In Prop y l2) (_ : forall _ : x, y), stronger l1 l2 *)
  intros l1 l2 x y Heq1 Heq2 HxIn HyIn Hxy x1 y1 Hx1In Hy1In.
(* Goal: forall _ : x1, y1 *)
  rewrite (Heq1 x1 x); [rewrite (Heq2 y1 y)|..]; assumption.
Qed.

Lemma stronger2__stronger_right : forall l1 l2 l2',
  stronger l1 l2 -> stronger l1 l2' -> stronger l1 (l2++l2').
Proof.
(* Goal: forall (l1 l2 l2' : list Prop) (_ : stronger l1 l2) (_ : stronger l1 l2'), stronger l1 (@app Prop l2 l2') *)
  intros l1 l2 l2' Hs Hs' x y Hx Hy.
(* Goal: iff x y *)
  apply in_app_or in Hy.
(* Goal: forall _ : x, y *)
  destruct Hy.
(* Goal: forall _ : x, y *)
(* Goal: forall _ : x, y *)
    apply Hs; assumption.
(* Goal: forall _ : x, y *)
    apply Hs'; assumption.
Qed.

Lemma stronger2__stronger_left : forall l1 l1' l2,
  stronger l1 l2 -> stronger l1' l2 -> stronger (l1++l1') l2.
Proof.
(* Goal: forall (l1 l1' l2 : list Prop) (_ : stronger l1 l2) (_ : stronger l1' l2), stronger (@app Prop l1 l1') l2 *)
  intros l1 l1' l2 Hs Hs' x y Hx Hy.
(* Goal: iff x y *)
  apply in_app_or in Hx.
(* Goal: forall _ : x, y *)
  destruct Hx.
(* Goal: forall _ : x, y *)
(* Goal: forall _ : x, y *)
    apply Hs; assumption.
(* Goal: forall _ : x, y *)
    apply Hs'; assumption.
Qed.

Lemma stronger_transitivity : forall l1 l2 l3,
  stronger l1 l2 -> stronger l2 l3 -> l2 <> nil -> stronger l1 l3.
Proof.
(* Goal: forall (l1 l2 l3 : list Prop) (_ : stronger l1 l2) (_ : stronger l2 l3) (_ : not (@eq (list Prop) l2 (@nil Prop))), stronger l1 l3 *)
  intros l1 l2 l3 Hs1 Hs2 Hl2 x z Hx Hz.
(* Goal: forall _ : x, z *)
  destruct l2.
(* Goal: forall _ : x, z *)
(* Goal: forall _ : x, z *)
    intuition.
(* Goal: forall _ : x, z *)
  unfold stronger in *.
(* Goal: forall _ : x, z *)
  specialize Hs1 with x P.
(* Goal: forall _ : x, z *)
  specialize Hs2 with P z.
(* Goal: forall _ : x, z *)
  simpl in *.
(* Goal: forall _ : x, z *)
  auto.
Qed.

Lemma all_equiv2_stronger2__all_equiv : forall l1 l2,
  all_equiv l1 -> all_equiv l2 ->
  stronger l1 l2 -> stronger l2 l1 ->
  all_equiv (l1++l2).
Proof.
(* Goal: forall (l1 l2 : list Prop) (_ : all_equiv l1) (_ : all_equiv l2) (_ : stronger l1 l2) (_ : stronger l2 l1), all_equiv (@app Prop l1 l2) *)
  intros l1 l2 He1 He2 Hs1 Hs2 x y Hx Hy.
(* Goal: iff x y *)
  apply in_app_or in Hx.
(* Goal: iff x y *)
  apply in_app_or in Hy.
(* Goal: iff x y *)
  destruct Hx; destruct Hy; auto; split.
(* Goal: forall _ : y, x *)
    apply Hs1; assumption.
(* Goal: forall _ : x, y *)
(* Goal: forall _ : y, x *)
    apply Hs2; assumption.
(* Goal: forall _ : x, y *)
(* Goal: forall _ : y, x *)
    apply Hs2; assumption.
(* Goal: forall _ : y, x *)
    apply Hs1; assumption.
Qed.

Lemma all_equiv3_stronger3__all_equiv : forall l1 l2 l3,
  l1 <> nil -> l2 <> nil -> l3 <> nil ->
  all_equiv l1 -> all_equiv l2 -> all_equiv l3 ->
  stronger l1 l2 -> stronger l2 l3 ->  stronger l3 l1 ->
  all_equiv (l1++l2++l3).
Proof.
(* Goal: forall (l1 l2 l3 : list Prop) (_ : not (@eq (list Prop) l1 (@nil Prop))) (_ : not (@eq (list Prop) l2 (@nil Prop))) (_ : not (@eq (list Prop) l3 (@nil Prop))) (_ : all_equiv l1) (_ : all_equiv l2) (_ : all_equiv l3) (_ : stronger l1 l2) (_ : stronger l2 l3) (_ : stronger l3 l1), all_equiv (@app Prop l1 (@app Prop l2 l3)) *)
  intros l1 l2 l3 H1 H2 H3 He1 He2 He3 Hs1 Hs2 Hs3.
(* Goal: all_equiv (@app Prop l1 (@app Prop l2 l3)) *)
  apply all_equiv2_stronger2__all_equiv.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    assumption.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply all_equiv2_stronger2__all_equiv; [..|apply stronger_transitivity with l1]; assumption.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply stronger2__stronger_right; [|apply stronger_transitivity with l2]; assumption.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply stronger2__stronger_left; [apply stronger_transitivity with l3|]; assumption.
Qed.

Lemma all_equiv2_impl2__all_equiv : forall l1 l2 x y x' y',
  all_equiv l1 -> all_equiv l2 ->
  In x l1 -> In y l2 -> (x -> y) ->
  In x' l2 -> In y' l1 -> (x' -> y') ->
  all_equiv (l1++l2).
Proof.
(* Goal: forall (l1 l2 : list Prop) (x y x' y' : Prop) (_ : all_equiv l1) (_ : all_equiv l2) (_ : @In Prop x l1) (_ : @In Prop y l2) (_ : forall _ : x, y) (_ : @In Prop x' l2) (_ : @In Prop y' l1) (_ : forall _ : x', y'), all_equiv (@app Prop l1 l2) *)
  intros l1 l2 x y x' y'; intros.
(* Goal: all_equiv (@app Prop l1 l2) *)
  apply all_equiv2_stronger2__all_equiv; trivial.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply all_equiv2_impl__stronger with x y; assumption.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply all_equiv2_impl__stronger with x' y'; assumption.
Qed.

Lemma all_equiv3_impl3__all_equiv : forall l1 l2 l3 x y x' y' x'' y'',
  all_equiv l1 -> all_equiv l2 -> all_equiv l3 ->
  In x l1 -> In y l2 -> (x -> y) ->
  In x' l2 -> In y' l3 -> (x' -> y') ->
  In x'' l3 -> In y'' l1 -> (x'' -> y'') ->
  all_equiv (l1++l2++l3).
Proof.
(* Goal: forall (l1 l2 l3 : list Prop) (x y x' y' x'' y'' : Prop) (_ : all_equiv l1) (_ : all_equiv l2) (_ : all_equiv l3) (_ : @In Prop x l1) (_ : @In Prop y l2) (_ : forall _ : x, y) (_ : @In Prop x' l2) (_ : @In Prop y' l3) (_ : forall _ : x', y') (_ : @In Prop x'' l3) (_ : @In Prop y'' l1) (_ : forall _ : x'', y''), all_equiv (@app Prop l1 (@app Prop l2 l3)) *)
  intros l1 l2 l3 x y x' y' x'' y''; intros.
(* Goal: all_equiv (@app Prop l1 (@app Prop l2 l3)) *)
  apply all_equiv3_stronger3__all_equiv; trivial; try (intro He; rewrite He in *; auto).
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply all_equiv2_impl__stronger with x y; assumption.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply all_equiv2_impl__stronger with x' y'; assumption.
(* Goal: all_equiv l1 *)
(* Goal: all_equiv (@app Prop l2 l3) *)
(* Goal: stronger l1 (@app Prop l2 l3) *)
(* Goal: stronger (@app Prop l2 l3) l1 *)
    apply all_equiv2_impl__stronger with x'' y''; assumption.
Qed.

Lemma all_equiv_trivial : forall x, all_equiv (x::nil).
Proof.
(* Goal: forall x : Prop, all_equiv (@cons Prop x (@nil Prop)) *)
  unfold all_equiv; simpl.
(* Goal: forall _ : or (@eq Prop x y) False, iff x0 y *)
  induction 1;[|contradiction].
(* Goal: forall _ : or (@eq Prop x y) False, iff x0 y *)
  induction 1;[|contradiction].
(* Goal: iff x0 y *)
  subst; reflexivity.
Qed.

Lemma incl_preserves_all_equiv : forall l1 l2,
  incl l1 l2 -> all_equiv l2 -> all_equiv l1.
Proof.
(* Goal: forall (l1 l2 : list Prop) (_ : @incl Prop l1 l2) (_ : all_equiv l2), all_equiv l1 *)
  unfold all_equiv.
(* Goal: forall _ : x, z *)
  intros; eauto.
Qed.

Lemma incl_preserves_stronger : forall l1 l2 l1' l2',
  incl l1 l1' -> incl l2 l2' -> stronger l1' l2' -> stronger l1 l2.
Proof.
(* Goal: forall (l1 l2 l1' l2' : list Prop) (_ : @incl Prop l1 l1') (_ : @incl Prop l2 l2') (_ : stronger l1' l2'), stronger l1 l2 *)
  intros l1 l2 l1' l2' Hi1 Hi2 Hs x y Hxl1 Hyl2.
(* Goal: forall _ : x, z *)
  apply Hs; auto.
Qed.

Ltac inlist := simpl; repeat (try (left; reflexivity); right).