Transitivity of Leibniz equality
Prove manually the following theorem (already in Coq's base of
theorems) :
forall (A:Set) (a b c:A), a = b -> b = c -> a = c.
- Applying explicitely eq_ind,
- Using Rewrite
Solution
Look at this file
Going home
Pierre Castéran