Vec 0の元は全部VNilであることの証明(see https://twitter.com/i/web/status/1027868640169717762)

Vec.v

Require Import JMeq.

Section Vec.
  Variable A:Set.
  Inductive Vec : nat -> Set :=
  | VNil : Vec O
  | VCons : forall n, A -> Vec n -> Vec (S n).

  Lemma Vec0_is_JMeq_to_VNil : forall n (v : Vec n),
    n = 0 -> JMeq v VNil.
  Proof.
    intros n v. destruct v.
    - reflexivity.
    - discriminate.
  Qed.

  Goal forall v : Vec 0, v = VNil.
  Proof.
    intros v. apply JMeq_eq.
    now apply Vec0_is_JMeq_to_VNil.
  Qed.

End Vec.

Vecの別証明.v

Section Vec.
  Variable A:Set.
  Inductive Vec : nat -> Set :=
  | VNil : Vec O
  | VCons : forall n, A -> Vec n -> Vec (S n).

  Goal forall v : Vec 0, v = VNil.
  Proof.
    intros v.
    refine(match v with
           | VNil => _
           | _ => _
           end).
    - reflexivity.
    - exact idProp.
  Qed.

End Vec.