ssreflect.v

Require Import ssreflect.
(*
Playing with 
https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#type-families
*)

Lemma foo {a1 a2} : a1 = a2 -> a1 + a1 = a2 + a2.
Fail progress case.

(* Either one works, and gives a goal that can be dispatches by reflexivity. *)

(* case E: _ /. *)
(* case E: a2 /.  *)
(* case: a2 /. *)

(* Harder: let's rewrite just one occurrence of a2, but generate an equation E: *)
case E: {2} a2 /.
(* Let's destruct on this equation to get to the rest. *)
(* case: a1 / E. *)
(* case: {1 2 3} a1 / E. *)
case: {1} a1 / E.
reflexivity.
Qed.