InductionStuck.v

Definition bounded_card (A: Type) (n: nat) := 
exists l, (forall a: A, In a l) /\ length l <= n.




 Lemma length_cand : forall {A : Type} n , 
      Fixpoints.bounded_card A n -> Fixpoints.bounded_card (A * A) (n * n).
  Proof.
    intros A n. unfold Fixpoints.bounded_card.
    intros [l H]. exists (all_pairs l).
    destruct H as [H1 H2]. split. 
    intros (a1, a2). clear H2. induction l.
    specialize (H1 a1). inversion H1.
    simpl. 
    pose proof H1 a1.
    destruct H as [H3 | H3].
    {
      pose proof H1 a2.
      destruct H as [H4 | H4].
      left. congruence.
      right. apply in_app_iff. right.
      apply in_app_iff. left.
      rewrite H3. apply in_map. assumption.
    }
    {
      pose proof H1 a2.
      destruct H as [H4 | H4].
      right. apply in_app_iff.
      right. apply in_app_iff.
      right. rewrite H4. apply in_map_iff.
      exists a1. split. auto. auto.
      right. apply in_app_iff. left.
      
      
       A : Type
  n : nat
  a : A
  l : list A
  H1 : forall a0 : A, In a0 (a :: l)
  a1, a2 : A
  IHl : (forall a : A, In a l) -> In (a1, a2) (all_pairs l)
  H3 : In a1 l
  H4 : In a2 l
  ============================
  In (a1, a2) (all_pairs l)