The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Good Night (midnight here),

I think you have an error in your example. Because trivial/reflexivity/auto... does the job. :/

Theorem my_theorem:forall (a b c: my_type),  (my_ind a b) = (my_ind b c) -> 2 = 2.
Proof.
  intros a b c H.
  reflexivity.
Qed.

Could you please elaborate a bit more what you are looking for.

Kind regards.

Benoît

2016-03-01 7:09 GMT+09:00 Kiarash Rahmani <rahmank AT purdue.edu>:

Hey all,

I am stuck in the middle of a proof. 

In assumptions, I have an equality of two inductively defined propositions, and I need to make use of it. Here is a toy example to explain it:

Inductive my_type : Type :=

  | one : my_type

  | two : my_type 

  | other : nat -> my_type.

 Inductive my_ind (a b:my_type) : my_type -> Prop :=

  | cons_introl :forall x: my_type, b = one  ->  my_ind a b x

  | cons_intror :forall x: my_type, a = one  ->  my_ind a b x.

Theorem my_theorem:forall (a b c: my_type),  (my_ind a b) =  (my_ind b c) -> 2=2.

Proof.

  intros a b c H.

  (*How sould I make use of H?   inversion, injection, unfold, does not seem to work*)

  (*I need to destruct two possible ways of constructing my_ind, and then prove the goal in each case*)

Abort.

Thank you very much