a new explanation
Induction.v done
proved few exercises