Changing well founded induction to fix on accessibility proof in order to  prepare the  possibility to  define  function with  more that  one argument.
Changing well founded induction to fix on accessibility proof in order
to  prepare the  possibility to  define  function with  more that  one
argument.


git-svn-id: 44dc50bdcc0f5d1a212c497508dc9452e0b35e2b@7856 85f007b7-540e-0410-9357-904b9bb8a0f7

mlasson/coq,maximedenes/coq,SkySkimmer/coq,asr/coq,william-lawvere/coq,pirapira/coq2rust,shindere/coq,letouzey/coq-wip,herbelin/coq-hh,aspiwack/coq,TheTypoMaster/coq,ale-f/coq,jpdeplaix/coq,barras/coq,letouzey/coq-wip,jhjourdan/coq,gmalecha/coq,letouzey/coq-wip,Matafou/coq,ppedrot/coq,pirbo/coq,coq/coq,asr/coq,amintimany/coq,william-lawvere/coq,Zimmi48/coq,herbelin/github-coq,TOSPIO/coq,asr/coq,shindere/coq,Zimmi48/coq,mattam82/coq,coq/coq,TOSPIO/coq,Zimmi48/coq,maximedenes/coq,ale-f/coq,ppedrot/coq,ejgallego/coq,Matafou/coq,TheTypoMaster/coq,maximedenes/coq,pirapira/coq2rust,ppedrot/coq,gmalecha/coq,silene/coq,ppedrot/coq,ejgallego/coq,tomprince/coq,mattam82/coq,JasonGross/coq,8l/coq,william-lawvere/coq,jpdeplaix/coq,shindere/coq,silene/coq,mlasson/coq,gares/coq,mattam82/Coq-misc,tomprince/coq,coq/coq,pirbo/coq,silene/coq,ppedrot/coq,ejgallego/coq,herbelin/coq-hh,JasonGross/coq,letouzey/coq-wip,ale-f/coq,JasonGross/coq,aspiwack/coq,gares/coq,Zimmi48/coq,amintimany/coq,gares/coq,jpdeplaix/coq,coq/coq,ejgallego/coq,jhjourdan/coq,gares/coq,Lionel-Rieg/coq,letouzey/coq-wip,TOSPIO/coq,maximedenes/coq,pirbo/coq,barras/coq,8l/coq,JasonGross/coq,Ptival/coq,SkySkimmer/coq,pirapira/coq2rust,mattam82/Coq-misc,barras/coq,Lionel-Rieg/coq,herbelin/github-coq,Lionel-Rieg/coq,8l/coq,Ptival/coq,gmalecha/coq,herbelin/github-coq,Matafou/coq,SkySkimmer/coq,aspiwack/coq,TheTypoMaster/coq,gares/coq,mlasson/coq,maximedenes/coq,amintimany/coq,tomprince/coq,mattam82/coq,SkySkimmer/coq,Ptival/coq,jhjourdan/coq