Proving a property on sets

Question

As a Coq programming experience and following my question in here, I'd like to know if there is another proof, possibly shorter and without using Lemma subset_listpair_conserve, for proving Lemma subset_listpair_consFalse. I proved it but it is long and uses Lemma subset_listpair_consve.

Require Import List.
Require Import Bool.

Definition entity := nat.
Definition entityID := nat.
Definition listPair : Set := list (entity * entityID).

(* check if e is in list l *)
Fixpoint in_listpair e (l : listPair) :=
  match l with
  | nil          => false
  | (x, y) :: l' => Nat.eqb e x || in_listpair e l'
  end.

(* check if list l1 is in list l2: i.e., 11 entities are in l2 *)
Fixpoint subset_listpair (l1 l2 : listPair) :=
  match l1 with
  | nil => true
  | (x1, _) :: l1 => in_listpair x1 l2 && subset_listpair l1 l2
  end.

Lemma subset_listpair_consver l1 l2 l3 e :
  in_listpair e l2 = true ->
  in_listpair e l3 = false ->
  subset_listpair l1 l2 = true ->
  subset_listpair l1 l3 = false.
l1, l2, l3: listPair
e: nat
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
Proof.
l1, l2, l3: listPair
e: nat
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
Admitted.

Lemma subset_listpair_consFalse l1 l2 l3 :
  subset_listpair l1 l2 = true ->
  subset_listpair l1 l3 = false -> subset_listpair l2 l3 = false.
l1, l2, l3: listPair
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
Proof.
l1, l2, l3: listPair
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
  induction l1.
l2, l3: listPair
subset_listpair nil l2 = true ->
subset_listpair nil l3 = false ->
subset_listpair l2 l3 = false
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
subset_listpair (a :: l1) l2 = true ->
subset_listpair (a :: l1) l3 = false ->
subset_listpair l2 l3 = false
  -
l2, l3: listPair
subset_listpair nil l2 = true ->
subset_listpair nil l3 = false ->
subset_listpair l2 l3 = false induction l3.
l2: listPair
subset_listpair nil l2 = true ->
subset_listpair nil nil = false ->
subset_listpair l2 nil = false
l2: listPair
a: (entity * entityID)%type
l3: list (entity * entityID)
IHl3: subset_listpair nil l2 = true ->
subset_listpair nil l3 = false ->
subset_listpair l2 l3 = false
subset_listpair nil l2 = true ->
subset_listpair nil (a :: l3) = false ->
subset_listpair l2 (a :: l3) = false
    +
l2: listPair
subset_listpair nil l2 = true ->
subset_listpair nil nil = false ->
subset_listpair l2 nil = false destruct l2.
subset_listpair nil nil = true ->
subset_listpair nil nil = false ->
subset_listpair nil nil = false
p: (entity * entityID)%type
l2: list (entity * entityID)
subset_listpair nil (p :: l2) = true ->
subset_listpair nil nil = false ->
subset_listpair (p :: l2) nil = false
      *
subset_listpair nil nil = true ->
subset_listpair nil nil = false ->
subset_listpair nil nil = false simpl.
true = true -> true = false -> true = false intros.
H: true = true
H0: true = false
true = false inversion H0.
      *
p: (entity * entityID)%type
l2: list (entity * entityID)
subset_listpair nil (p :: l2) = true ->
subset_listpair nil nil = false ->
subset_listpair (p :: l2) nil = false intros.
p: (entity * entityID)%type
l2: list (entity * entityID)
H: subset_listpair nil (p :: l2) = true
H0: subset_listpair nil nil = false
subset_listpair (p :: l2) nil = false destruct p.
e: entity
e0: entityID
l2: list (entity * entityID)
H: subset_listpair nil ((e, e0) :: l2) = true
H0: subset_listpair nil nil = false
subset_listpair ((e, e0) :: l2) nil = false simpl in *.
e: entity
e0: entityID
l2: list (entity * entityID)
H: true = true
H0: true = false
false = false reflexivity.
    +
l2: listPair
a: (entity * entityID)%type
l3: list (entity * entityID)
IHl3: subset_listpair nil l2 = true ->
subset_listpair nil l3 = false ->
subset_listpair l2 l3 = false
subset_listpair nil l2 = true ->
subset_listpair nil (a :: l3) = false ->
subset_listpair l2 (a :: l3) = false simpl in *.
l2: listPair
a: (entity * entityID)%type
l3: list (entity * entityID)
IHl3: true = true ->
true = false -> subset_listpair l2 l3 = false
true = true ->
true = false -> subset_listpair l2 (a :: l3) = false intros.
l2: listPair
a: (entity * entityID)%type
l3: list (entity * entityID)
IHl3: true = true ->
true = false -> subset_listpair l2 l3 = false
H: true = true
H0: true = false
subset_listpair l2 (a :: l3) = false intuition.
l2: listPair
l3: list (entity * entityID)
H: true = true
H0: true = false
a0: entity
b: entityID
H2: subset_listpair l2 l3 = false
subset_listpair l2 ((a0, b) :: l3) = false inversion H0.
  -
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
subset_listpair (a :: l1) l2 = true ->
subset_listpair (a :: l1) l3 = false ->
subset_listpair l2 l3 = false intros.
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
subset_listpair l2 l3 = false rewrite IHl1.
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
false = false
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
subset_listpair l1 l2 = true
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
subset_listpair l1 l3 = false
    +
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
false = false reflexivity.
    +
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
subset_listpair l1 l2 = true simpl in H0.
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: (let (x1, _) := a in
 in_listpair x1 l3 && subset_listpair l1 l3) =
false
subset_listpair l1 l2 = true destruct a.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair ((e, e0) :: l1) l2 = true
H0: in_listpair e l3 && subset_listpair l1 l3 = false
subset_listpair l1 l2 = true simpl in H.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 && subset_listpair l1 l2 = true
H0: in_listpair e l3 && subset_listpair l1 l3 = false
subset_listpair l1 l2 = true
      rewrite andb_true_iff in H.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 && subset_listpair l1 l3 = false
subset_listpair l1 l2 = true rewrite andb_false_iff in H0.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
subset_listpair l1 l2 = true
      elim H.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
in_listpair e l2 = true ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l2 = true intros.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
subset_listpair l1 l2 = true assumption.
    +
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: subset_listpair (a :: l1) l3 = false
subset_listpair l1 l3 = false simpl in H0.
a: (entity * entityID)%type
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair (a :: l1) l2 = true
H0: (let (x1, _) := a in
 in_listpair x1 l3 && subset_listpair l1 l3) =
false
subset_listpair l1 l3 = false destruct a.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: subset_listpair ((e, e0) :: l1) l2 = true
H0: in_listpair e l3 && subset_listpair l1 l3 = false
subset_listpair l1 l3 = false simpl in H.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 && subset_listpair l1 l2 = true
H0: in_listpair e l3 && subset_listpair l1 l3 = false
subset_listpair l1 l3 = false
      rewrite andb_true_iff in H.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 && subset_listpair l1 l3 = false
subset_listpair l1 l3 = false rewrite andb_false_iff in H0.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
subset_listpair l1 l3 = false
      elim H.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
in_listpair e l2 = true ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false intros.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
subset_listpair l1 l3 = false
      *
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
subset_listpair l1 l3 = false elim H0.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
in_listpair e l3 = false ->
subset_listpair l1 l3 = false
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
subset_listpair l1 l3 = false ->
subset_listpair l1 l3 = false
        --
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
in_listpair e l3 = false ->
subset_listpair l1 l3 = false intros.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
subset_listpair l1 l3 = false pose proof subset_listpair_consver as H10.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
subset_listpair l1 l3 = false
           assert (subset_listpair l1 l3 = false) as H11.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
subset_listpair l1 l3 = false
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
H11: subset_listpair l1 l3 = false
subset_listpair l1 l3 = false
           ++
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
subset_listpair l1 l3 = false rewrite H10 with (l2 := l2) (e := e).
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
false = false
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
in_listpair e l2 = true
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
in_listpair e l3 = false
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
subset_listpair l1 l2 = true
              **
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
false = false reflexivity.
              **
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
in_listpair e l2 = true assumption.
              **
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
in_listpair e l3 = false assumption.
              **
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
subset_listpair l1 l2 = true assumption.
           ++
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: in_listpair e l3 = false
H10: forall (l1 l2 l3 : listPair) (e : nat),
in_listpair e l2 = true ->
in_listpair e l3 = false ->
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false
H11: subset_listpair l1 l3 = false
subset_listpair l1 l3 = false assumption.
        --
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
subset_listpair l1 l3 = false ->
subset_listpair l1 l3 = false intro.
e: entity
e0: entityID
l1: list (entity * entityID)
l2, l3: listPair
IHl1: subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
H: in_listpair e l2 = true /\
subset_listpair l1 l2 = true
H0: in_listpair e l3 = false \/
subset_listpair l1 l3 = false
H1: in_listpair e l2 = true
H2: subset_listpair l1 l2 = true
H3: subset_listpair l1 l3 = false
subset_listpair l1 l3 = false assumption.
Qed.

Answer

Here is one possible solution. I didn't go for a lemma-less proof or for the shortest proof. Instead, I tried to break down everything into a bite-sized chunks that are (relatively) easy to manipulate.

First, here is an auxiliary lemma missing from the standard library. It simply states the law of contraposition in classical logic (we have decidable propositions here, so those are kind of classical).

From Coq Require Import Arith Bool List.

Lemma contra b1 b2 :
  (b2 = false -> b1 = false) <-> (b1 = true -> b2 = true).
b1, b2: bool
(b2 = false -> b1 = false) <->
(b1 = true -> b2 = true)
Proof.
b1, b2: bool
(b2 = false -> b1 = false) <->
(b1 = true -> b2 = true) destruct b1, b2; intuition. Qed.

Now, we will need the following easy property:

Lemma in_subset_listpair {p l1 l2} :
  in_listpair p l1 = true ->
  subset_listpair l1 l2 = true ->
  in_listpair p l2 = true.
p: nat
l1, l2: listPair
in_listpair p l1 = true ->
subset_listpair l1 l2 = true ->
in_listpair p l2 = true
Proof.
p: nat
l1, l2: listPair
in_listpair p l1 = true ->
subset_listpair l1 l2 = true ->
in_listpair p l2 = true
  induction l1 as [| [x1 y1] l1 IH]; simpl; [easy |].
p: nat
x1: entity
y1: entityID
l1: list (entity * entityID)
l2: listPair
IH: in_listpair p l1 = true ->
subset_listpair l1 l2 = true ->
in_listpair p l2 = true
(p =? x1) || in_listpair p l1 = true ->
in_listpair x1 l2 && subset_listpair l1 l2 = true ->
in_listpair p l2 = true
  rewrite orb_true_iff, andb_true_iff.
p: nat
x1: entity
y1: entityID
l1: list (entity * entityID)
l2: listPair
IH: in_listpair p l1 = true ->
subset_listpair l1 l2 = true ->
in_listpair p l2 = true
(p =? x1) = true \/ in_listpair p l1 = true ->
in_listpair x1 l2 = true /\
subset_listpair l1 l2 = true ->
in_listpair p l2 = true intros [->%Nat.eqb_eq |] []; trivial.
p: nat
x1: entity
y1: entityID
l1: list (entity * entityID)
l2: listPair
IH: in_listpair p l1 = true ->
subset_listpair l1 l2 = true ->
in_listpair p l2 = true
H: in_listpair p l1 = true
H0: in_listpair x1 l2 = true
H1: subset_listpair l1 l2 = true
in_listpair p l2 = true
  now apply IH.
Qed.

Next, we prove that subset is transitive:

Lemma subset_listpair_transitive l2 l1 l3 :
  subset_listpair l1 l2 = true ->
  subset_listpair l2 l3 = true ->
  subset_listpair l1 l3 = true.
l2, l1, l3: listPair
subset_listpair l1 l2 = true ->
subset_listpair l2 l3 = true ->
subset_listpair l1 l3 = true
Proof.
l2, l1, l3: listPair
subset_listpair l1 l2 = true ->
subset_listpair l2 l3 = true ->
subset_listpair l1 l3 = true
  induction l1 as [| [x1 y1] l1 IH]; simpl; trivial.
l2: listPair
x1: entity
y1: entityID
l1: list (entity * entityID)
l3: listPair
IH: subset_listpair l1 l2 = true ->
subset_listpair l2 l3 = true ->
subset_listpair l1 l3 = true
in_listpair x1 l2 && subset_listpair l1 l2 = true ->
subset_listpair l2 l3 = true ->
in_listpair x1 l3 && subset_listpair l1 l3 = true
  intros [I1 S1]%andb_prop S2.
l2: listPair
x1: entity
y1: entityID
l1: list (entity * entityID)
l3: listPair
IH: subset_listpair l1 l2 = true ->
subset_listpair l2 l3 = true ->
subset_listpair l1 l3 = true
I1: in_listpair x1 l2 = true
S1: subset_listpair l1 l2 = true
S2: subset_listpair l2 l3 = true
in_listpair x1 l3 && subset_listpair l1 l3 = true rewrite (IH S1 S2), andb_true_r.
l2: listPair
x1: entity
y1: entityID
l1: list (entity * entityID)
l3: listPair
IH: subset_listpair l1 l2 = true ->
subset_listpair l2 l3 = true ->
subset_listpair l1 l3 = true
I1: in_listpair x1 l2 = true
S1: subset_listpair l1 l2 = true
S2: subset_listpair l2 l3 = true
in_listpair x1 l3 = true
  now apply (in_subset_listpair I1).
Qed.

And now, the target lemma, which is basically a contrapositive statement of the transitivity property:

Lemma subset_listpair_consFalse l1 l2 l3 :
  subset_listpair l1 l2 = true ->
  subset_listpair l1 l3 = false ->
  subset_listpair l2 l3 = false.
l1, l2, l3: listPair
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
Proof.
l1, l2, l3: listPair
subset_listpair l1 l2 = true ->
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false
  intros S12.
l1, l2, l3: listPair
S12: subset_listpair l1 l2 = true
subset_listpair l1 l3 = false ->
subset_listpair l2 l3 = false rewrite contra.
l1, l2, l3: listPair
S12: subset_listpair l1 l2 = true
subset_listpair l2 l3 = true ->
subset_listpair l1 l3 = true
  now apply subset_listpair_transitive.
Qed.