[PVS-Help] some problems about list which is provided by the prelude

[applehopedream <applehopedream@xxxxxxx>]

 Hello,

 

     If I use cons(a,cons(b,null) in my file ,I know using length(cons(a,cons(b,null)) can get the length of the list,but  I want to get the length in the prove that is using prover command gets the real value ,2.How could I do?Thank you !

 

 

 

---

22元超值饭面,8.5折纯珍比萨,必胜宅急送网上点餐优惠多