coq-club AT inria.fr

Subject: The Coq mailing list

List archive

How can I prove this?

Theorem T m:
(fix F n m := match n with O => match m with O => O | _ => O end | S n' => S n' + F n' m end) O m = m.

Thanks in advance,

Ilmars

[Coq-Club] Rewriting inside fixpoint, Ilmārs Cīrulis, 12/03/2013
- Re: [Coq-Club] Rewriting inside fixpoint, Beta Ziliani, 12/03/2013
  - [Coq-Club] Fwd: Rewriting inside fixpoint, Beta Ziliani, 12/03/2013
- Re: [Coq-Club] Rewriting inside fixpoint, Vincent, 12/03/2013
  - Re: [Coq-Club] Rewriting inside fixpoint, Ilmārs Cīrulis, 12/04/2013
    - Re: [Coq-Club] Rewriting inside fixpoint, Ilmārs Cīrulis, 12/04/2013
      - Re: [Coq-Club] Rewriting inside fixpoint, Rui Baptista, 12/04/2013
        
        Re: [Coq-Club] Rewriting inside fixpoint, Ilmārs Cīrulis, 12/04/2013
        
        Re: [Coq-Club] Rewriting inside fixpoint, Ilmārs Cīrulis, 12/04/2013
        
        Re: [Coq-Club] Rewriting inside fixpoint, Adam Chlipala, 12/04/2013
        Re: [Coq-Club] Rewriting inside fixpoint, Cedric Auger, 12/04/2013