phantoms types and logic proving at compile time in c# v2

Phantom.cs

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

class Program
{
    static void Main(string[] args)
    {
        var lst = SafeListMethods.Create<String>();
        var lst2 = lst.Add("aaa", L.False);
        
        var lst4 = lst2
            //.Add(null, L.True)// if uncomment compile fails
            .Print().Print();// bad but every print removes "head"
        L.AsserTrue(lst4.IsListEmpty());//assert at compile time
        Console.ReadKey();

    }
}

    static class L
    {
        //prove logical expressions at compile time
        public static void Test()
        {
            var a1 = Not(And(False, Not(True)));
            var a2 = Not(And(False, True));
            TTrue t = Equivalent(a1, a2);

            L.AsserTrue(Equivalent(Zero, Zero.Add().Minus()));
        }


        public static TTrue True { get; private set; }
        public static TFalse False { get; private set; }
        public static Zero Zero { get; private set; }
        
        public static TTrue And(this TTrue t, TTrue t2)
        {
            throw new Exception();
        }
        public static TFalse And(this TFalse t, TTrue t2)
        {
            throw new Exception();
        }
        public static TFalse And(this TTrue t, TFalse t2)
        {
            throw new Exception();
        }
        public static TFalse And(this TFalse t, TFalse t2)
        {
            throw new Exception();
        }

        public static TTrue Or(this TTrue t, TTrue t2)
        {
            throw new Exception();
        }
        public static TTrue Or(this TTrue t, TFalse t2)
        {
            throw new Exception();
        }
        public static TTrue Or(this TFalse t, TTrue t2)
        {
            throw new Exception();
        }
        public static TFalse Or(this TFalse t, TFalse t2)
        {
            throw new Exception();
        }

        public static TTrue Not(this TFalse t)
        {
            throw new Exception();
        }

        public static TFalse Not(this TTrue t)
        {
            throw new Exception();
        }

        public static TTrue Implies(this TTrue t, TTrue t2)
        {
            throw new Exception();
        }
        public static TFalse Implies(this TTrue t, TFalse t2)
        {
            throw new Exception();
        }
        public static TTrue Implies(this TFalse t, TTrue t2)
        {
            throw new Exception();
        }
        public static TTrue Implies(this TFalse t, TFalse t2)
        {
            throw new Exception();
        }

        public static TTrue Equivalent<T>(this T t, T t2)
        {
            throw new Exception();
        }

        public static Succ<Zero> Add(this Zero zero)
        {
            throw new Exception();
        }
        public static Succ<Succ<T>> Add<T>(this Succ<T> number)
        {
            throw new Exception();
        }
        public static Zero Minus(this Succ<Zero> zero)
        {
            throw new Exception();
        }
        public static Succ<T> Minus<T>(this Succ<Succ<T>> number)
        {
            throw new Exception();
        }

        public static void AsserTrue(TTrue t)
        {
            
        }

        public static void AsserFalse(TFalse t)
        {
            
        }
        
    }


class Succ<T>
{
    public int Value()
    {
        return this.ToString().Split('S').Length;
    }
}

class Zero
{

    public int Value()
    {
        return 0;
    }
}


class TTrue
{
    public bool Value()
    {
        return true;
    }
}
class TFalse
{
    public bool Value()
    {
        return false;
    }
}

    class SafeList<T, Length, ContainsNulls> {
        private SafeList()
        {

        }
        public List<T> lst = null;

        public static SafeList<T, Zero, TFalse> Create<T>()
        {
            return new SafeList<T, Zero, TFalse> { lst = new List<T>() };
        }

        public SafeList<T, ToLength, ToContainsNulls> Cast<ToLength, ToContainsNulls>()
        {
            return new SafeList<T, ToLength, ToContainsNulls> { lst = this.lst};
        }
    }

    static class SafeListMethods
    {
        public static SafeList<T, Zero, TFalse> Create<T>()
        {
            return SafeList<T, Zero, TFalse>.Create<T>();
        }

        public static TTrue IsListEmpty<T, ContainsNulls>(this SafeList<T, Zero, ContainsNulls> lst)
        {
            return new TTrue();
        }
        public static TFalse IsListEmpty<T, T2, ContainsNulls>(this SafeList<T, Succ<T2>, ContainsNulls> lst)
        {
            return new TFalse();
        }
        public static TFalse ContainsNulls<T, T2>(this SafeList<T, T2, TFalse> lst)
        {
            return new TFalse();
        }

        public static TTrue ContainsNulls<T, T2>(this SafeList<T, T2, TTrue> lst)
        {
            return new TTrue();
        }

        public static SafeList<T, Succ<Length>, TTrue> Add<T, Length>(this SafeList<T, Length, TTrue> lst, T item)
        {
            lst.lst.Add(item);
            return lst.Cast<Succ<Length>, TTrue>(); 
        }

        public static SafeList<T, Succ<Length>, TTrue> Add<T, Length>(this SafeList<T, Length, TFalse> lst, T item, TTrue itemIsNull)
        {
            lst.lst.Add(item);
            return lst.Cast<Succ<Length>, TTrue>(); 
        }

        public static SafeList<T, Succ<Length>, TFalse> Add<T, Length>(this SafeList<T, Length, TFalse> lst, T item, TFalse itemIsNull)
        {
            lst.lst.Add(item);
            return lst.Cast<Succ<Length>, TFalse>(); 
        }

        public static T Head<T, T2, ContainsNulls>(this SafeList<T, Succ<T2>, ContainsNulls> lst)
        {
            return lst.lst[lst.lst.Count-1];
        }

        public static SafeList<T, T2, ContainsNulls> GetTail<T, T2, ContainsNulls>(this SafeList<T, Succ<T2>, ContainsNulls> lst)
        {
            lst.lst.RemoveAt(lst.lst.Count-1);// doto immutable list
            return lst.Cast<T2, ContainsNulls>(); 
        }

        public static SafeList<T, T2, TFalse> Print<T, T2>(this SafeList<T, Succ<T2>, TFalse> lst)
        {
            Console.WriteLine(lst.Head().ToString());
            var nLst = lst.GetTail();
            return nLst;
        }

        public static SafeList<T, Zero, TFalse> Print<T>(this SafeList<T, Zero, TFalse> lst)
        {
            Console.WriteLine("Finished");
            return lst;
        }

    }